Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions

By Yves Bertot, P. Castran. 2010

1,770 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/f04af7291d49a0912def77a432b9ad79baa2096d

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs (2020, background): “The declarative feature (i.e. focusing on intermediate propositions) was then incorporated into other systems including HOL Light [51], Isabelle [50], and Coq [15].”
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, methodology): “Like Coq and HOL Light, also Isabelle [14] was used for major formalization e ﬀ orts, such as the formalization of the seL4 microkernel [16].”
A Formal Foundation for Secure Remote Execution of Enclaves (2017, methodology): “[69] used the Coq proof assistant [8] to verify correctness of a multiprocessor directory-based cache coherence protocol.”
Programming Puzzles (2021, background): “Several neighboring fields that have made substantial progress in reasoning include theorem prov357 ing [6], two-player game playing [53], and SAT-solving [7].”
A Formally Verified Compiler Back-end (2009, methodology): “This verification is mechanized using the Coq proof assistant [25,11].”
Abstractions for network update (2012, methodology): “In addition to the proof sketch included in this paper, this result has been formally verified in the Coq proof assistant [12].”
Formal Proof—The Four- Color Theorem (2008, background): “The Coq code (available at the same address) is the ultimate reference for the intrepid, who should bone up on Coq [4] [16] [9] beforehand.”
Formal verification of a realistic compiler (2009, methodology): “This paper gives a high-level overview of the CompCert compiler and its mechanized verification, which uses the Coq proof assistant [7, 3].”
A Natural Proof System for Natural Language (2017, methodology): “Their inference system CCG2λ is implemented in a proof-assistant Coq (Bertot et al., 2010), which augments the first-order inference of Coq with additional axioms and inference tactics for natural logic constructions.”
HyperTree Proof Search for Neural Theorem Proving (2022, background): “However, these approaches are insufficient when it comes to theorems written in modern proof assistants such as Isabelle [13], Coq [14], or Lean [4].”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, methodology): “Furthermore, although it maintains internally a single proof representation, cvc5 is able to emit proofs in multiple formats, including those supported by the LFSC [133] proof checker and the Lean 4 [88], Isabelle/HOL [100] and Coq [30] proof assistants.”
Rodin: an open toolset for modelling and reasoning in Event-B (2010, methodology): “Powerful theorem provers are available [14,19,26, 36] but not enough attention has been paid in formal methods to tool support for the modelling activity per se.”
Refinement types for Haskell (2014, background): ““Full” dependently typed systems like Coq [6], Agda [29], and Idris [8] typically use structural checks where recursion is allowed on sub-terms of ADTs to ensure that all terms terminate.”
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, methodology): “This work directly depends on Lean’s mathlib , but indirectly beneﬁts from lessons learned from other proofs systems such as Coq [Bertot and Castéran, 2004], Mizar [Grabowski et al., 2010], and Isabelle [Nipkow et al., 2002].”