The \textsc{MetaCoq} project
From MaRDI portal
Publication:2209542
DOI10.1007/s10817-019-09540-0zbMath1468.68075OpenAlexW2953833525MaRDI 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
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (8)
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 ⋮ Extracting functional programs from Coq, in Coq ⋮ Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version ⋮ Unnamed Item ⋮ MetaCoq ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory
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]
This page was built for publication: The \textsc{MetaCoq} project
