Types for Proofs and Programs

DOI10.1007/11617990zbMath1172.68414OpenAlexW4300050167MaRDI 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

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Related Items (7)

Verified abstract interpretation techniques for disassembling low-level self-modifying code ⋮ Certified Static Analysis by Abstract Interpretation ⋮ A formally verified compiler back-end ⋮ Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves ⋮ Program and proof optimizations with type systems ⋮ Building Certified Static Analysers by Modular Construction of Well-founded Lattices ⋮ Structural Abstract Interpretation: A Formal Study Using Coq

This page was built for publication: Types for Proofs and Programs