A Short Presentation of Coq
From MaRDI portal
Publication:3543643
DOI10.1007/978-3-540-71067-7_3zbMATH Open1165.68449OpenAlexW1857315623MaRDI QIDQ3543643FDOQ3543643
Authors: 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
Recommendations
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- scientific article; zbMATH DE number 1070623
- scientific article; zbMATH DE number 6296049
- scientific article; zbMATH DE number 512790
- Synthesis of ML programs in the system Coq
Cites Work
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- An introduction to small scale reflection in Coq
- Verifying Nonlinear Real Formulas Via Sums of Squares
- The calculus of constructions
- Synthesis of ML programs in the system Coq
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formal certification of a compiler back-end or
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
Cited In (13)
- Validating QBF Validity in HOL4
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- An introduction to programming and proving with dependent types in Coq
- Truth, Proof, and Reproducibility: There’s No Counter-Attack for the Codeless
- Machine learning guidance for connection tableaux
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A formal study of Bernstein coefficients and polynomials
- An introduction to small scale reflection in Coq
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- A compact kernel for the calculus of inductive constructions
- Deductive Binary Code Verification Against Source-Code-Level Specifications
- Psi-calculi in Isabelle
- Hammer for Coq: automation for dependent type theory
Uses Software
This page was built for publication: A Short Presentation of Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3543643)
