A Short Presentation of Coq

DOI10.1007/978-3-540-71067-7_3zbMath1165.68449OpenAlexW1857315623MaRDI QIDQ3543643

Yves Bertot

Publication date: 4 December 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71067-7_3

Mathematics Subject Classification ID

Related Items

Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation, Hammer for Coq: automation for dependent type theory, Psi-calculi in Isabelle, Truth, Proof, and Reproducibility: There’s No Counter-Attack for the Codeless, Machine learning guidance for connection tableaux, Validating QBF Validity in HOL4, A formal study of Bernstein coefficients and polynomials, Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The calculus of constructions
• Synthesis of ML programs in the system Coq
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Formal certification of a compiler back-end or