Interactive Theorem Proving and Program Development

By Yves Bertot, P. Castéran. Texts in Theoretical Computer Science. An EATCS Series, 2004

1,147 citations recorded by the source corpus.

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

How researchers see this paper

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

In Artificial Intelligence

Citations in the corpus

Why3: Shepherd Your Herd of Provers (2011, background): “Proof assistants such as Coq [6], PVS [25], or Isabelle [17] also provide rich speciﬁcation languages that are convenient to model programs.”
A Brief Overview of Agda - A Functional Language with Dependent Types (2009, background): “The most well-known system with dependent types which is based on the Curry-Howard identiﬁcation is Coq [2].”
Mechanized Metatheory for the Masses: The PoplMark Challenge (2005, background): “However, despite much encouraging progress in recent years and the availability of several mature tools (ACL2 [26], Coq [3], HOL [18], HOL Light [21], Isabelle [35], Lego [28], NuPRL [7], PVS [40], Twelf [42], etc.”
From program verification to program synthesis (2010, background): “Using significant human input, theorems proved interactively in the Coq have a computational analog that can be extracted [2].”
A Classification and Survey of Analysis Strategies for Software Product Lines (2014, background): “Interactive theorem provers, such as COQ [Bertot and Castéran 2004], PVS [Owre et al. 1992], and ISABELLE/HOL [Nipkow et al. 2002], require the user to write commands applying inference rules.”
Homotopy theoretic models of identity types (2007, background): “[2] and [4]), this promise of applications is of a practical, as well as theoretical, nature.”
Map fusion for nested datatypes in intensional type theory (2011, background): “Programming with nested datatypes is possible in the functional programming language Haskell (and Haskell is the language in which the example programs of [1] and many other papers since then, up to the recent [7], are presented), but this article is concerned with frameworks that guarantee terminat”
Formal verification of a realistic compiler (2009, background): “Having proved properties (2) or ( 3 ) provides the same guarantee without having to equip the target and intermediate languages with sound type systems and to prove type preservation for the compiler.”