The \textsc{MetaCoq} project
From MaRDI portal
Publication:2209542
DOI10.1007/s10817-019-09540-0zbMath1468.68075MaRDI QIDQ2209542
Abhishek Anand, Simon Boulier, Nicolas Tabareau, Cyril Cohen, Matthieu Sozeau, Yannick Forster, Gregory Malecha, Fabian Kunze, Théo Winterhalter
Publication date: 2 November 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-019-09540-0
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Related Items
Extracting functional programs from Coq, in Coq, Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version, MetaCoq, \texttt{slepice}: towards a verified implementation of type theory in type theory, Reasoning about iteration and recursion uniformly based on big-step semantics, Translation certification for smart contracts, Formal analysis of the application programming interface of the PVS verification system
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Canonicity of weak \(\omega\)-groupoid laws using parametricity theory
- MetaML and multi-stage programming with explicit annotations
- Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9--12, 2018. Proceedings
- Weak call-by-value lambda calculus as a model of computation in Coq
- Towards certified meta-programming with typed Template-Coq
- HOL Light QE
- Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}
- Extensible and Efficient Automation Through Reflective Tactics
- Type Theory Should Eat Itself
- Type theory in type theory using quotient inductive types
- Proofs for free
- A compiled implementation of strong reduction
- Elaborator reflection: extending Idris in Idris
- The Definitional Side of the Forcing
- Efficient self-interpretation in lambda calculus
- Program-ing finger trees in C <scp>oq</scp>
- Typed syntactic meta-programming
- Mtac: A monad for typed tactic programming in Coq
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- Programming in the λ-Calculus: From Church to Scott and Back
- Extending Coq with Imperative Features and Its Application to SAT Verification
- [https://portal.mardi4nfdi.de/wiki/Publication:5875425 A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus]
