Verification of the interface of a small proof system in Coq
From MaRDI portal
Recommendations
- Proof by computation in the Coq system
- A proof system for MSVL programs in Coq
- Formal verification of cP systems using Coq
- Verification of dynamic bisimulation theorems in Coq
- Verifying object-oriented programs with higher-order separation logic in Coq
- Small Witnesses for Abstract Interpretation-Based Proofs
- Modular SMT proofs for fast reflexive checking inside Coq
- A Coq library for verification of concurrent programs
- Program verification by coinduction
- A mechanized proof system of the third generation calculus in Coq
Cited in
(14)- A compact kernel for the calculus of inductive constructions
- Formalizing generalized maps in Coq
- Formalizing the trading theorem in Coq
- A solution to the PoplMark challenge based on de Bruijn indices
- A formalization and proof checker for Isabelle's metalogic
- Strongly reducing variants of the Krivine abstract machine
- Towards a formally verified proof assistant
- A mechanized proof system of the third generation calculus in Coq
- The challenge of computer mathematics
- Pure type systems with explicit substitutions
- Computer Science Logic
- Extending Coq with Imperative Features and Its Application to SAT Verification
- \textsf{LOGIC}: a Coq library for logics
- Soundness of the Q0 proof system for higher-order logic
This page was built for publication: Verification of the interface of a small proof system in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4246942)
