Collection

Tag: coq

Coq and the Curry-Howard Path from Proofs to Verified Programs

Coq turned constructive type theory into an interactive proof environment where mathematical proofs become machine-checkable terms and verified programs can be extracted from formal developments.

↗

CompCert and the Verified Compiler: Proving the Translator Correct

CompCert used Coq to prove semantic preservation across a realistic optimizing C compiler, closing the assurance gap between verified source programs and generated assembly.

↗