Coq support in HAHA

DOI10.4230/LIPICS.TYPES.2016.8MaRDI QIDQ6855249zbMATH OpenFDO

Authors Jacek Chrząszcz, Aleksy Schubert, Jakub Zakrzewski

Publication date 20 February 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2016.8

zbMATH Keywords

Coq theorem proverHoare logicprogram verificationteaching

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• A formally verified compiler back-end
• An axiomatic basis for computer programming
• Characteristic formulae for the verification of imperative programs
• Coinductive big-step operational semantics
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• Why3 -- where programs meet provers

This page was built for publication: Coq support in HAHA

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6855249)