Proofs of randomized algorithms in Coq (2009)
Audebaud, Philippe, Paulin-Mohring, Christine
Randomized algorithms are widely used for finding efficiently approximated solutions to complex problems, for instance primality testing and for obtaining good average behavior. Proving properties of...
A constructive denotational semantics for Kahn networks in Coq (2009)
Semantics of programming languages and interactive environments for the development of proofs and programs are two important aspects of Gilles Kahn's scientific contributions. In his paper ``The...
Proofs of randomized algorithms in Coq (2009)
Audebaud, Philippe, Paulin-Mohring, Christine
Randomized algorithms are widely used for finding efficiently approximated solutions to complex problems, for instance primality testing and for obtaining good average behavior. Proving properties of...
A constructive denotational semantics for Kahn networks in Coq (2009)
Semantics of programming languages and interactive environments for the development of proofs and programs are two important aspects of Gilles Kahn's scientific contributions. In his paper ``The...
Christine Paulin-mohring, Marc He, Outlineffl Intro
W arningfflKraka to a is based on the
Ecole Normale, Suprieure Lyon, Adresses Lectroniques, Christine Paulin-mohring
In the pure Calculus of Constructions, it is possible to represent data structures and predicates using higher-order quantification. However, this representation is not satisfactory, from the point...
A constructive denotational semantics for Kahn networks in Coq (2007)
Christine Paulin-mohring, Inria Futurs
Semantics of programming languages and interactive environments for the development of proofs and programs are two important aspects of Gilles Kahn’s scientific contributions. In his paper “The...
The Coq Proof Assistant : A Tutorial : Version 7.2 (2002)
Huet, Gérard, Kahn, Gilles, Paulin-Mohring, Christine
Coq is a proof assistant based on a higher-order logic. Coq allows to handle calculus mathematical assertions and to check mechanically proofs of these assertions. It helps to find formal proofs, and...
The Coq Proof Assistant : A Tutorial : Version 7.2 (2002)
Huet, Gérard, Kahn, Gilles, Paulin-Mohring, Christine
Coq is a proof assistant based on a higher-order logic. Coq allows to handle calculus mathematical assertions and to check mechanically proofs of these assertions. It helps to find formal proofs, and...
The Coq Proof Assistant : A Tutorial : Version 7.2 (2002)
Huet, Gérard, Kahn, Gilles, Paulin-Mohring, Christine
Coq is a proof assistant based on a higher-order logic. Coq allows to handle calculus mathematical assertions and to check mechanically proofs of these assertions. It helps to find formal proofs, and...
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 : A Tutorial : Version 6.1 (1997)
Huet, Gérard, Kahn, Gilles, Paulin-Mohring, Christine
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. This document is a tutorial for the version V6.1 of Coq. This version is available by anonymous ftp...
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 : A Tutorial : Version 6.1 (1997)
Huet, Gérard, Kahn, Gilles, Paulin-Mohring, Christine
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. This document is a tutorial for the version V6.1 of Coq. This version is available by anonymous ftp...
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 : A Tutorial : Version 6.1 (1997)
Huet, Gérard, Kahn, Gilles, Paulin-Mohring, Christine
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. This document is a tutorial for the version V6.1 of Coq. This version is available by anonymous ftp...
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...
Définitions Inductives en Théorie des Types (1996)
Ce document donne un panorama de la représentation des définitions inductives dans différents assistants de preuve en logique d'ordre supérieur, théorie des ensembles et théorie des types. Il...
Définitions Inductives en Théorie des Types (1996)
Ce document donne un panorama de la représentation des définitions inductives dans différents assistants de preuve en logique d'ordre supérieur, théorie des ensembles et théorie des types. Il...
Définitions Inductives en Théorie des Types (1996)
Ce document donne un panorama de la représentation des définitions inductives dans différents assistants de preuve en logique d'ordre supérieur, théorie des ensembles et théorie des types. Il...
Circuits as streams in COQ: verification of a sequential multiplier. (1995)
(eng) This paper presents the proof of correctness of a multiplier circuit formalized in the calculus of inductive constructions. It uses a representation of the circuit as a function from the stream...
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 user's guide : version 5.8 (1993)
Dowek, Gilles, Felty, Amy, Herbelin, H., Parent, Catherine, Paulin-Mohring, Christine, ...
The Coq proof assistant user's guide : version 5.8 (1993)
Dowek, Gilles, Felty, Amy, Herbelin, H., Huet, Gerard, Parent, Catherine, Paulin-Mohring, Christine, ...
pas de résumé
The Coq proof assistant user's guide : version 5.8 (1993)
Dowek, Gilles, Felty, Amy, Herbelin, H., Huet, Gerard, Parent, Catherine, Paulin-Mohring, Christine, ...
pas de résumé
The Coq proof assistant user's guide : version 5.6 (1991)
Dowek, Gilles, Felty, Amy, Herbelin, H., Huet, Gerard, Werner, Benjamin, Paulin-Mohring, Christine
pas de resume
The Coq proof assistant user's guide : version 5.6 (1991)
Dowek, Gilles, Felty, Amy, Herbelin, H., Huet, Gerard, Werner, Benjamin, Paulin-Mohring, Christine
pas de resume
Inductively defined types in the calculus of constructions (1990)
Frank Pfenning, Christine Paulin-mohring
We define the notion of an inductively defined type in the Calculus of Constructions and show how inductively defined types can be represented by closed types. We show that all primitive recursive...
Extraction de programmes dans le Calcul des Constructions (1989)
Cette thèse propose une extension du Calcul des Constructions de Coquand et Huet qui permet l'extraction de programmes certifiés à partir de preuve constructive. Une notion de réalisabilité...
Extraction de programmes dans le Calcul des Constructions (1989)
Cette thèse propose une extension du Calcul des Constructions de Coquand et Huet qui permet l'extraction de programmes certifiés à partir de preuve constructive. Une notion de réalisabilité...
Extraction de programmes dans le Calcul des Constructions (1989)
Cette thèse propose une extension du Calcul des Constructions de Coquand et Huet qui permet l'extraction de programmes certifiés à partir de preuve constructive. Une notion de réalisabilité...