Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
No abstract available.
DOI 10.1007/978-3-540-71316-6_15
Related papers
- Proof-producing translation of higher-order logic into pure and stateful ML JFP 2014
- Proof-producing synthesis of ML from higher-order logic ICFP 2012
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement ESOP 2017
- Compositional optimizations for CertiCoq ICFP 2021
- A Lambda-Superposition Tactic for Isabelle/HOL CPP 2026
- Higher-Order Specifications for Deductive Synthesis of Programs with Pointers ECOOP 2024
- Extending a Brainiac Prover to Lambda-Free Higher-Order Logic TACAS 2019
- Verifying a hash table and its iterators in higher-order separation logic CPP 2017