Correctly compiling proofs about programs without proving compilers correct

DOI10.4230/LIPICS.ITP.2024.33MaRDI QIDQ6859994zbMATH OpenFDO

Authors Audrey Seo, Christopher Lam, Dan Grossman, Talia Ringer

Publication date 10 February 2026

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

program logicsproof engineeringproof transformationscompiler validation

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 1696821 (Why is no real title available?)
• A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
• ANF preserves dependent types up to extensional equality
• Abstraction and subsumption in modular verification of C programs
• CakeML
• Changing data representation within the \textsf{Coq} system
• Characteristic formulae for the verification of imperative programs
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Interactive proofs in higher-order concurrent separation logic
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Mechanized semantics for the clight subset of the C language
• Metamath Zero: designing a theorem prover prover
• On the completeness of propositional Hoare logic
• Refinement to imperative HOL
• Theorem Proving in Higher Order Logics
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Ynot: dependent types for imperative programs

This page was built for publication: Correctly compiling proofs about programs without proving compilers correct

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