Höpner, Martin, Petring, Alexander, Seikel, Daniel, Werner, Benjamin
Liberalisierungspolitik bezeichnet die politisch herbeigeführte und politisch legitimierte Delegation von Allokations- und Distributionsentscheidungen an Märkte und zielt auf Durchsetzung der...
Projet LogiCal P^ole Commun de Recherche en Informatique du Plateau de Saclay' (2008)
constructive logic
Projet LogiCal P^ole Commun de Recherche en Informatique du Plateau de Saclay' (2008)
Abstract. We present constructive arithmetic in Deduction modulo with rewrite rules only. In natural deduction and in sequent calculus, the cut elimination theoremand the analysis of the structure of...
On the strength of proof-irrelevant type theories (2008)
We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlying a theorem...
Une Théorie des Constructions Inductives (2008)
L'objet de cette thèse est la méta-théorie du Calcul des Constructions Inductives (CCI), c'est à dire les Calcul des Constructions étendu par des types et des prédicats inductifs. Le Calcul des...
Une Théorie des Constructions Inductives (2007)
L'objet de cette thèse est la méta-théorie du Calcul des Constructions Inductives (CCI), c'est à dire les Calcul des Constructions étendu par des types et des prédicats inductifs. Le Calcul des...
Une Théorie des Constructions Inductives (2007)
L'objet de cette thèse est la méta-théorie du Calcul des Constructions Inductives (CCI), c'est à dire les Calcul des Constructions étendu par des types et des prédicats inductifs. Le Calcul des...
La Vérité et la Machine (2006)
En quelques pages nous présentons des avancées récentes où l'ordinateur permet d'établir des vérités mathématiques.
La Vérité et la Machine (2006)
En quelques pages nous présentons des avancées récentes où l'ordinateur permet d'établir des vérités mathématiques.
A computational approach to pocklington certificates in type theory (2006)
Benjamin Grégoire, Laurent Théry, Benjamin Werner
Abstract. Pocklington certificates are known to provide short proofs of primality. We show how to perform this in the framework of formal, mechanically checked, proofs. We present an encoding of...
Arithmetic as a theory modulo (2005)
Abstract. We present constructive arithmetic in Deduction modulo with rewrite rules only. In natural deduction and in sequent calculus, the cut elimination theorem and the analysis of the structure...
Green Bank Telescope Penn Array Project Leader at Penn (2005)
Benjamin Werner, Dr. Simon Dicker
The Experimental Cosmology Group at the University Pennsylvania is finishing the development of a telescope receiver that will operate at 90 GHz, a frequency in the far infrared band. This receiver...
Choice in dynamic linking (2004)
Martín Abadi, Georges Gonthier, Benjamin Werner
Abstract. We introduce a computational interpretation for Hilbert’s choice operator (ε). This interpretation yields a typed foundation for dynamic linking in software systems. The use of choice...
Proof normalization modulo (2003)
Dowek, Gilles, Werner, Benjamin
We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories having a...
B.: The not so simple proof-irrelevant model of CC (2002)
Abstract. It is well-known that the Calculus of Constructions (CC) bears a simple set-theoretical model in which proof-terms are mapped onto a single object—a property which is known as...
B.: The not so simple proof-irrelevant model of CC (2002)
Abstract. It is well-known that the Calculus of Constructions (CC) bears a simple set-theoretical model in which proof-terms are mapped onto a single object—a property which is known as...
Proof Normalization Modulo (1998)
Dowek, Gilles, Werner, Benjamin
We consider a class of logical formalisms, in which first-order logic is extended by identifying propositions modulo a given congruence. We particularly focus on the case where this congruence is...
A Generic Normalisation Proof for Pure Type Systems (1998)
Melliès, Paul-André, Werner, Benjamin
We prove the strong normalisation for any PTS, provided the existence of a certain $\Lambda$-set $\A for every sort s of the system. The properties verified by the $\A's depend of the axioms and...
Proof Normalization Modulo (1998)
Dowek, Gilles, Werner, Benjamin
We consider a class of logical formalisms, in which first-order logic is extended by identifying propositions modulo a given congruence. We particularly focus on the case where this congruence is...
A Generic Normalisation Proof for Pure Type Systems (1998)
Melliès, Paul-André, Werner, Benjamin
We prove the strong normalisation for any PTS, provided the existence of a certain $\Lambda$-set $\A for every sort s of the system. The properties verified by the $\A's depend of the axioms and...
Proof Normalization Modulo (1998)
Dowek, Gilles, Werner, Benjamin
We consider a class of logical formalisms, in which first-order logic is extended by identifying propositions modulo a given congruence. We particularly focus on the case where this congruence is...
A Generic Normalisation Proof for Pure Type Systems (1998)
Melliès, Paul-André, Werner, Benjamin
We prove the strong normalisation for any PTS, provided the existence of a certain $\Lambda$-set $\A for every sort s of the system. The properties verified by the $\A's depend of the axioms and...
The Coq Proof Assistant Reference Manual (1998)
Jean-christophe Filliatre, Hugo Herbelin, Bruno Barras, Bruno Barras, Samuel Boutin, Samuel Boutin, ...
apport technique
Proof Normalization Modulo (1998)
Gilles Dowek, Gilles Dowek, Benjamin Werner, Benjamin Werner
We consider a class of logical formalisms, in which first-order logic is extended by identifying propositions modulo a given congruence. We particularly focus on the case where this congruence is...
Proof normalization modulo (1998)
Abstract. We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories...
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...
Sets in Types, Types in Sets (1997)
. We present two mutual encodings, respectively of the Calculus of Inductive Constructions in Zermelo-Fraenkel set theory and the opposite way. More precisely, we actually construct two families of...
. 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....
A Generic Normalisation Proof for Pure Type Systems (1996)
Paul-André Melliès, Benjamin Werner
We prove the strong normalisation for any PTS, provided the existence of a certain-set A * (s) for every sort s of the system. The properties verified by the A * (s)'s depend of the axiom and...
A Generic Normalisation Proof for Pure Type Systems (1996)
Paul-André Melliès, Benjamin Werner
We prove the strong normalisation for any PTS, provided the existence of a certain-set A * (s) for every sort s of the system. The properties verified by the A * (s)'s depend of the axiom 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
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...
Une Théorie des Constructions Inductives (1994)
L'objet de cette thèse est la méta-théorie du Calcul des Constructions Inductives (CCI), c'est à dire les Calcul des Constructions étendu par des types et des prédicats inductifs. Le Calcul des...
Une Théorie des Constructions Inductives (1994)
L'objet de cette thèse est la méta-théorie du Calcul des Constructions Inductives (CCI), c'est à dire les Calcul des Constructions étendu par des types et des prédicats inductifs. Le Calcul des...
Une Théorie des Constructions Inductives (1994)
L'objet de cette thèse est la méta-théorie du Calcul des Constructions Inductives (CCI), c'est à dire les Calcul des Constructions étendu par des types et des prédicats inductifs. Le Calcul des...
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é
On the Definition of the Eta-long Normal Form in Type Systems of the Cube (1993)
The smallest transitive relation ! on well-typed normal terms such that if t is a strict subterm of u then t ! u and if T is the normal form of the type of t and the term t is not a sort then T ! t...
On the Definition of the Eta-long Normal Form in Type Systems of the Cube (1993)
The smallest transitive relation ! on well-typed normal terms such that if t is a strict subterm of u then t ! u and if T is the normal form of the type of t and the term t is not a sort then T ! t...