Procédures De Décisions Dans Les Systèmes Avec Types Dépendants (2007)
Introduction Dans ce papier, nous ne parlons que des syst`emes d'aide `a la d'emonstration bas'es sur la th'eorie des types. Le probl`eme de l'existence de proc'edures...
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...
Using Reflection to Build Efficient and Certified Decision Procedures (1997)
In this paper we explain how computational reflection can help build efficient certified decision procedure in reduction systems. We have developped a decision procedure on abelian rings in the Coq...
In this report we show how we proved correctness of the translation from a small applicative language with recursive definitions (Mini-ML) to the Categorical abstract machine (CAM) using the Coq...
In this report we show how we proved correctness of the translation from a small applicative language with recursive definitions (Mini-ML) to the Categorical abstract machine (CAM) using the Coq...
In this report we show how we proved correctness of the translation from a small applicative language with recursive definitions (Mini-ML) to the Categorical abstract machine (CAM) using the Coq...
In this article we show how we proved correctness of the translation from a small applicative language with recursive definitions (Mini-ML) to the Categorical abstract machine (CAM) using the Coq...
Calcul Symbolique, Samuel Boutin, Samuel Boutin, Projet Coq
Machine). Notre objectif a 'et'e de m'ecaniser une preuve pr'esent'ee dans l'article de J. Despeyroux [9] et 'ecrite `a l'aide du langage Typol. Nous utilisons...