coq-in-coq
Compiler verification project
A formalization of a theoretical programming language in Coq to verify its correctness and extract a certified compiler
A formalisation of the Calculus of Constructions
66 stars
13 watching
7 forks
Language: Coq
last commit: 7 months ago