Coq to C Translation with Partial Evaluation + Counterexample Generation
summary
Builds a verified Coq-to-C code generator that uses a custom codogen plugin and a partial-evaluation pipeline to monomorphize polymorphic/dependent functions, emit tail-recursive loops as goto-based C, map inductive types to uint64/macros, and apply restricted beta/data reductions that avoid duplicated computation; prototype produces C functions provably equal to their Coq originals. The verification tool work produces ownership slicing and CHC-based counterexample traces for CONSORT-style ownership refinement types using an SMT backend (Z3), fast on small benchmarks (<1s) but slow on larger examples (>1min), prototype only.
AI-written summary · about
chapters (20)
- 0:00Introduction
- 1:05Coq to C purpose
- 2:55Low-level features
- 5:03Monadic power example
- 8:18Verifying translated code
- 9:03Partial evaluation
- 12:40Duplication in evaluation
- 17:01Convergence rules
- 19:10Normal form terms
- 25:18Combining evaluation and verification
- 26:06Q&A on monomorphization
- 31:32Second talk intro
- 32:16Consul verification overview
- 34:01Consul demo sorted list
- 36:14Consul error limits
- 37:58Hybrid error messages
- 42:40Type inference slicing
- 45:55Counterexample generation
- 51:58Related work and conclusion
- 53:46Q&A on scalability
related talks
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
24mFormally Verified Native Code Generation in an Effectful JIT: Turning the CompCe...
58mFast Cryptographic Code via Partial Evaluation
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
19mInterpreting OCaml GADTs into Coq
24mCode Extraction from Coq to ML-like languages
19mExtensible Metatheory Mechanization via Family Polymorphism
15mCompiling with Continuations, Correctly