Docteur En Informatique, Boris Yakobowski, Roberto Di Cosmo, Stéphanie Weirich, Hugo Herbelin, ...
pour obtenir le titre de
Boris Yakobowski, Roberto Di Cosmo, Stéphanie Weirich, Hugo Herbelin, Fritz Henglein, ...
présentée à
Kripke Models for Classical Logic (2009)
Ilik, Danko, Lee, Gyesik, Herbelin, Hugo
We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.
Kripke Models for Classical Logic (2009)
Ilik, Danko, Lee, Gyesik, Herbelin, Hugo
We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.
Kripke Models for Classical Logic (2009)
Ilik, Danko, Lee, Gyesik, Herbelin, Hugo
We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.
Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus (2009)
We give a simple intuitionistic completeness proof of Kripke semantics for intuitionistic logic with implication and universal quantification with respect to cut-free intuitionistic sequent calculus....
Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus (2009)
We give a simple intuitionistic completeness proof of Kripke semantics for intuitionistic logic with implication and universal quantification with respect to cut-free intuitionistic sequent calculus....
Herbelin, Hugo, Zimmermann, Stéphane
We give a decomposition of the equational theory of call-by-value lambda-calculus into a confluent rewrite system made of three independent subsystems that refines Moggi's computational calculus: -...
Herbelin, Hugo, Zimmermann, Stéphane
We give a decomposition of the equational theory of call-by-value lambda-calculus into a confluent rewrite system made of three independent subsystems that refines Moggi's computational calculus: -...
Kripke Models for Classical Logic (2009)
Ilik, Danko, Lee, Gyesik, Herbelin, Hugo
We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.
Kripke Models for Classical Logic (2009)
Ilik, Danko, Lee, Gyesik, Herbelin, Hugo
We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.
Abstract. The work presented here is an extension of a previous work realised jointly with Pierre-Louis Curien [1]. The title has been kept unchanged. The current work focuses on the pure calculus of...
We show that a variant of Parigot’s λµ-calculus, originally due to de Groote and proved to satisfy Böhm’s theorem by Saurin, is canonically interpretable as a call-by-name calculus of...
Investigations into the duality of computation (2008)
The work presented here is an extension of a previous work realised jointly with Pierre-Louis Curien [CH00]. The current work focuses on the pure calculus of variables and binders that operates at...
On the Degeneracy of Σ-Types in Presence of Computational Classical Logic (2008)
Hugo Herbelin, École Polytechnique
Abstract. We show that a minimal dependent type theory based on Σtypes and equality is degenerated in presence of computational classical logic. By computational classical logic is meant a classical...
Abstract machines for dialogue games (2007)
Curien, Pierre-Louis, Herbelin, Hugo
The notion of abstract Boehm tree has arisen as an operationally-oriented distillation of works on game semantics, and has been investigated in two papers. This paper revisits the notion, providing...
A Type-Theoretic Foundation of Delimited Continuations (2007)
Ariola, Zena, Herbelin, Hugo, Sabry, Amr
There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters, the continuations become composable and the...
Control Reduction Theories: the Benefit of Structural Substitution (2007)
The historical design of the call-by-value theory of control relies on the reification of evaluation contexts as regular functions and on the use of ordinary term application for jumping to a...
A Type-Theoretic Foundation of Delimited Continuations (2007)
Ariola, Zena, Herbelin, Hugo, Sabry, Amr
There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters, the continuations become composable and the...
Control Reduction Theories: the Benefit of Structural Substitution (2007)
The historical design of the call-by-value theory of control relies on the reification of evaluation contexts as regular functions and on the use of ordinary term application for jumping to a...
Abstract machines for dialogue games (2006)
Curien, Pierre-Louis, Herbelin, Hugo
The notion of abstract Boehm tree has arisen as an operationally-oriented distillation of works on game semantics, and has been investigated in two papers. This paper revisits the notion, providing...
Abstract machines for dialogue games (2006)
Curien, Pierre-Louis, Herbelin, Hugo
The notion of abstract Boehm tree has arisen as an operationally-oriented distillation of works on game semantics, and has been investigated in two papers. This paper revisits the notion, providing...
A. Stump, H. Xi, Thorsten Altenkirch, Hugo Herbelin, Simon Peyton-jones, Y Pollack, ...
The main goal of PLPV is to bring together researchers exploring language-based approaches to program verification. Typically in these approaches, the programming language provides mechanisms which...
Zena M. Ariola, Hugo Herbelin, Amr Sabry, Zena M. Ariola, Hugo Herbelin, Amr Sabry
We give an analysis of various classical axioms and characterize a notion of minimal classical logic that enforces Peirce’s law without enforcing Ex Falso Quodlibet. We show that a “natural ”...
Minimal Classical Logic and Control Operators (2003)
We give an analysis of various classical axioms and characterize a notion of minimal classical logic that enforces Peirce's law without enforcing Ex Falso Quodlibet. We show that a...
Explicit Substitutions and Reducibility (2001)
Abstract. We consider reducibility sets dened not by induction on types but by induction on sequents as a tool to prove strong normalization of systems with explicit substitution. To illustrate this...
Explicit Substitutions and Reducibility (2001)
We consider reducibility sets defined not by induction on types but by induction on sequents as a tool to prove strong normalization of systems with explicit substitution. To illustrate this point,...
The duality of computation (2000)
Herbelin, Hugo, Curien, Pierre-Louis
We present the lambda-bar-mu-mu-tilde-calculus, a syntax for lambda-calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived...
The duality of computation (2000)
Herbelin, Hugo, Curien, Pierre-Louis
We present the lambda-bar-mu-mu-tilde-calculus, a syntax for lambda-calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived...
The Duality of Computation (2000)
Pierre-Louis Curien, Hugo Herbelin
We present the ~-calculus, a syntax for -calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived from implicational...
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...
Games and Weak-Head Reduction for Classical PCF (1997)
We present a game model for classical PCF, a finite version of PCF extended by a catch/throw mechanism. This model is built from E-dialogues, a kind of two-players game defined by Lorenzen. In the...
Games and Weak-Head Reduction for Classical PCF (1997)
We present a game model for classical PCF, a finite version of PCF extended by a catch/throw mechanism. This model is built from E-dialogues, a kind of two-players game defined by Lorenzen. In the...
A-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure (1995)
. We consider a -calculus for which applicative terms have no longer the form (:::((u u1) u2 )::: un) but the form (u [u1 ; :::; un ]), for which [u1 ; :::; un ] is a list of terms. While the...
L'objet de cette thèse est l'étude des systèmes formels du type des systèmes LJ et LK de Gentzen (couramment appelés calculs des séquents) dans leur rapport avec la calculabilité. Le procédé...
L'objet de cette thèse est l'étude des systèmes formels du type des systèmes LJ et LK de Gentzen (couramment appelés calculs des séquents) dans leur rapport avec la calculabilité. Le procédé...
L'objet de cette thèse est l'étude des systèmes formels du type des systèmes LJ et LK de Gentzen (couramment appelés calculs des séquents) dans leur rapport avec la calculabilité. Le procédé...
L'objet de cette thèse est l'étude des systèmes formels du type des systèmes LJ et LK de Gentzen (couramment appelés calculs des séquents) dans leur rapport avec la calculabilité. Le procédé...
A-Translation and Looping Combinators in Pure Type Systems (1994)
Coquand, Thierry, Herbelin, Hugo
We present here a generalization of A-translation to a class of Pure Type Systems. We apply this translation to give a direct proof of the existence of a looping combinator in a large class of...
A-Translation and Looping Combinators in Pure Type Systems (1994)
Coquand, Thierry, Herbelin, Hugo
We present here a generalization of A-translation to a class of Pure Type Systems. We apply this translation to give a direct proof of the existence of a looping combinator in a large class of...
A-translation and Looping Combinators in Pure Type Systems (1994)
Thierry Coquand, Hugo Herbelin
We present here a generalization of A-translation to a class of Pure Type Systems. We apply this translation to give a direct proof of the existence of a looping combinator in a large class of...
A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure (1994)
We consider a lambda-calculus for which applicative terms have no longer the form (...((u u_1) u_2) ... u_n) but the form (u [u_1 ; ... ; u_n]), for which [u_1 ; ... ; u_n] is a list of terms. While...
A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure (1994)
We consider a lambda-calculus for which applicative terms have no longer the form (...((u u_1) u_2) ... u_n) but the form (u [u_1 ; ... ; u_n]), for which [u_1 ; ... ; u_n] is a list of terms. While...
Games and weak-head reduction for classical PCF (1990)
Abstract. We present a game model for classical PCF, a finite version of PCF extended by a catch/throw mechanism. This model is build from E-dialogues, a kind of two-players game defined by Lorenzen....