×

CertiCoq

swMATH ID: 22728
Software Authors: Anand, A., Appel, A., Morrisett, G., Paraskevopoulou, Z., Pollack, R., Belanger, O.S., Sozeau, M., Weaver, M.
Description: CertiCoq: a verified compiler for Coq. The CertiCoq project aims to build a proven-correct compiler for dependently-typed, functional languages, such as Gallina—the core language of the Coq proof assistant. A proved-correct compiler consists of a high-level functional specification, machine-verified proofs of important properties, such as safety and correctness, and a mechanism to transport those proofs to the generated machine code. The project exposes both engineering challenges and foundational questions about compilers for dependently-typed languages.
Homepage: https://www.cs.princeton.edu/~appel/certicoq/
Related Software: Coq; CakeML; Isabelle/HOL; OEuf; HOL; Fiat; Idris; Haskell; CompCert; Template-Coq; Mtac; Milawa; Isabelle; OpenTheory; MetaCoq; HOL Light QE; CoLoR; Jitawa; GRAT; HOL-TestGen
Cited in: 13 Publications

Citations by Year