Touring the MetaCoq project
From MaRDI portal
Cites work
- A machine-checked proof of the odd order theorem
- A new approach to incremental cycle detection and related problems
- An effectful way to eliminate addiction to dependence
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Canonicity for cubical type theory
- Cumulative inductive types in Coq
- Extending Coq with Imperative Features and Its Application to SAT Verification
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- scientific article; zbMATH DE number 1223720 (Why is no real title available?)
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- scientific article; zbMATH DE number 1088050 (Why is no real title available?)
- scientific article; zbMATH DE number 2003158 (Why is no real title available?)
- scientific article; zbMATH DE number 7649967 (Why is no real title available?)
- scientific article; zbMATH DE number 7699441 (Why is no real title available?)
- Parallel reductions in \(\lambda\)-calculus
- Primitive Floats in Coq
- Program logics for certified compilers
- Pure type system conversion is always typable
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Subset Coercions in Coq
- The \textsc{MetaCoq} project
- The calculus of constructions
- The definitional side of the forcing
- The verified CakeML compiler backend
- Towards Self-verification of HOL Light
- Type theory should eat itself
- Universe polymorphism in Coq
This page was built for publication: Touring the MetaCoq project
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6940481)
