Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}

DOI10.1145/3706056MaRDI QIDQ6854558zbMATH OpenFDO

Authors Matthieu Sozeau, Yannick Forster, Jakob Nielsen, Nicolas Tabareau, Théo Winterhalter

Publication date 24 February 2026

Published in Journal of the ACM (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1145/3706056

zbMATH Keywords

certificationproof assistantstype checker

Mathematics Subject Classification ID

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

Cites work

• A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus
• A new approach to incremental cycle detection and related problems
• A verified compiler from Isabelle/HOL to CakeML
• An effectful way to eliminate addiction to dependence
• Automata, Languages and Programming
• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• Candle: a verified implementation of HOL light
• Constructing recursion operators in intuitionistic type theory
• Copatterns, programming infinite structures by observations
• Cumulative inductive types in Coq
• Explicit substitutions
• Extracting functional programs from Coq, in Coq
• F-ing modules
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• scientific article; zbMATH DE number 2185666 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• scientific article; zbMATH DE number 2003158 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• scientific article; zbMATH DE number 7699441 (Why is no real title available?)
• Induction-recursion and initial algebras.
• Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism
• On equivalence and canonical forms in the LF type theory
• Parallel reductions in \(\lambda\)-calculus
• Proof-irrelevant model of CC with predicative induction and judgmental equality
• Proof-producing translation of higher-order logic into pure and stateful ML
• Pure type system conversion is always typable
• The calculus of constructions
• The Implicit Calculus of Constructions as a Programming Language with Dependent Types
• The view from the left
• Towards a formally verified proof assistant
• Towards certified meta-programming with typed Template-Coq
• Type checking with universes
• Universe polymorphism in Coq

Cited in

(1)

• A mechanized first-order theory of algebraic data types with pattern matching

This page was built for publication: Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}

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