Strong Normalization with Singleton Types Abstract (2008)
This paper presents a new lambda-calculus with singleton types, called λ βδ The main novelty of λ βδ ≤{} is the introduction of a new reduction, the δ-reduction, replacing any variable...
Strong Normalization with Singleton Types Abstract (2008)
This paper presents a new lambda-calculus with singleton types, called λ βδ The main novelty of λ βδ ≤{} is the introduction of a new reduction, the δ-reduction, replacing any variable...
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...
A Module Calculus for Pure Type Systems (1997)
. Several proof-assistants rely on the very formal basis of Pure Type Systems (PTS). However, some practical issues raised by the development of large proofs lead to add other features to actual...
A Module Calculus for Pure Type Systems (1997)
Several proof-assistants rely on the very formal basis of Pure Type Systems (PTS) as their foundations. We are concerned with the issues involved in the development of large proofs in these provers...
A Module Calculus for Pure Type Systems (1996)
Judicael Courant October, Judicaël Courant
Several proof-assistants rely on the very formal basis of Pure Type Systems. However, some practical issues raised by the development of large proofs lead to add other features to actual...
Proof reconstruction Preliminary version (1996)
Spike Coq, Judicaël Courant, Judicael Courant, Judicael Courant
In the field of formal methods, rewriting techniques and provers by consistency in particular appear as powerful tools for automating deduction. However, these provers suffer limitations as they only...
The Coq Proof Assistant, Reference Manual, Version 5.10 (1995)
Cornes, Cristina, Courant, Judicaël, Filliatre, Jean-Christophe, Huet, Gerard, Manoury, Pascal, Munoz, César, ...
The Coq Proof Assistant, Reference Manual, Version 5.10 (1995)
Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Huet, Gerard, Manoury, Pascal, Munoz, César, ...
Résumé disponible dans les fichiers attachés
The Coq Proof Assistant, Reference Manual, Version 5.10 (1995)
Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Huet, Gerard, Manoury, Pascal, Munoz, César, ...
Résumé disponible dans les fichiers attachés
The Coq Proof Assistant - Reference Manual V 5.10 (1995)
Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Gérard Huet, Chetan Murthy, César Muñoz, ...
ion All Axiom Begin Cd Chapter Check CheckGuard CoFixpoint Compute Defined Definition Drop Elimination End Eval Explain Extraction Fact Fixpoint Focus for Go Goal Hint Hypothesis Immediate Induction...