The Implicit Calculus of Constructions as a Programming Language with Dependent Types (2008)
Barras, Bruno, Bernardo, Bruno
In this paper, we show how Miquel's Implicit Calculus of Constructions (ICC) can be used as a programming language featuring dependent types. Since this system has an undecidable type-checking, we...
The Implicit Calculus of Constructions as a Programming Language with Dependent Types (2008)
Barras, Bruno, Bernardo, Bruno
In this paper, we show how Miquel's Implicit Calculus of Constructions (ICC) can be used as a programming language featuring dependent types. Since this system has an undecidable type-checking, we...
The Implicit Calculus of Constructions as a Programming Language with Dependent Types (2007)
Barras, Bruno, Bernardo, Bruno
In this paper, we show how Miquel's Implicit Calculus of Constructions (ICC) can be used as a programming language featuring dependent types. Since this system has an undecidable type-checking, we...
The Implicit Calculus of Constructions as a Programming Language with Dependent Types (2007)
Barras, Bruno, Bernardo, Bruno
In this paper, we show how Miquel's Implicit Calculus of Constructions (ICC) can be used as a programming language featuring dependent types. Since this system has an undecidable type-checking, we...
On the role of type decorations in the Calculus of Inductive Constructions (2005)
Bruno Barras, Benjamin Gregoire
In proof systems like Coq [15], proof-checking involves comparing types modulo #-conversion, which is potentially a time-consuming task. Significant speed-ups are achieved by compiling proof terms,...
The Coq Proof Assistant Reference Manual (1998)
Jean-christophe Filliatre, Hugo Herbelin, Bruno Barras, Bruno Barras, Samuel Boutin, Samuel Boutin, ...
apport technique
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
. We formalize the definition and the metatheory of the Calculus of Constructions (CC) using the proof assistant Coq. In particular, we prove strong normalization and decidability of type inference....
. We formalize the definition and the metatheory of the Calculus of Constructions (CC) using the proof assistant Coq. In particular, we prove strong normalization and decidability of type inference....
The essential step of the formal verification of a proof-checker such as Coq is the verification of its kernel: a type-checker for the Calculus of Inductive Constructions (CIC) which is its...
The essential step of the formal verification of a proof-checker such as Coq is the verification of its kernel: a type-checker for the Calculus of Inductive Constructions (CIC) which is its...
The essential step of the formal verification of a proof-checker such as Coq is the verification of its kernel: a type-checker for the Calculus of Inductive Constructions (CIC) which is its...