scientific article; zbMATH DE number 1301729

MaRDI QIDQ4246942zbMATH OpenFDO

Authors Bruno Barras

Publication date 13 December 1999

zbMATH Keywords

calculus of constructionsformalization of the interface of a proof-checkerproofs-as-terms principletype system

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

Describes a project that uses

Uses Software

• Coq

This page was built for publication:

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