7 events
when toggle format what by license comment
Jan 21 at 23:10 comment added jmite You might also like this paper: dl.acm.org/doi/10.1145/3158111
Jan 12 at 20:28 comment added while1fork @paulotorrens So contrary to my assumptions, there is very little gap between paper proofs of normalization and formalized ones? Thanks.
Jan 12 at 9:00 history tweeted twitter.com/StackCSTheory/status/1481189233658376192
Jan 12 at 6:11 comment added paulotorrens Are you aware of the Coq in Coq paper? It formalizes the strong normalization proof for the calculus of constructions.
Jan 11 at 23:36 history edited while1fork CC BY-SA 4.0
added 139 characters in body
S Jan 11 at 23:18 review First questions
Jan 12 at 3:36
S Jan 11 at 23:18 history asked while1fork CC BY-SA 4.0