Synthesizing proofs from programs in the Calculus of Inductive Constructions (2007)
Ecole Normale, Suprieure Lyon, Catherine Parent December, Catherine Parent
Unit de recherche associe au CNRS n1398
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...
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
Synthesizing proofs from programs in the Calculus of Inductive Constructions (1995)
. We want to prove "automatically" that a program is correct with respect to a set of given properties that is a specification. Proofs of specifications contain logical parts and...
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...
The Coq proof assistant user's guide : version 5.8 (1993)
Dowek, Gilles, Felty, Amy, Herbelin, H., Parent, Catherine, Paulin-Mohring, Christine, ...