coq-in-coq
Type system compiler
A formalization of a type system's metatheory and proof-checker code in Coq, providing verified type inference and normalization.
A formalisation of the Calculus of Constructions
66 stars
13 watching
7 forks
Language: Coq
last commit: 4 months ago