Types for Proofs and Programs
From MaRDI portal
Publication:5898173
DOI10.1007/11617990zbMath1172.68414MaRDI QIDQ5898173
Benjamin Grégoire, Yves Bertot, Xavier Leroy
Publication date: 13 November 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11617990
68N20: Theory of compilers and interpreters
Related Items
Structural Abstract Interpretation: A Formal Study Using Coq, Building Certified Static Analysers by Modular Construction of Well-founded Lattices, Verified abstract interpretation techniques for disassembling low-level self-modifying code, Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves, Program and proof optimizations with type systems, A formally verified compiler back-end, Certified Static Analysis by Abstract Interpretation