Research articles

Abstract: We show that by restricting Martin-Löf's strong existential elimination (i.e. elimination of dependent sums) to "negative-elimination-free" proofs, one obtains a constructive logic that proves the axiom of dependent choice in a way that remains compatible with classical logic.

Abstract: It has been shown by Saurin that de Groote's variant of Parigot's lambda-mu-calculus is strictly more expressive in the untyped case than Parigot's original calculus. We show that this additional expressivity exactly corresponds to adding delimited control so that de Groote's calculus can be seen as the exact call-by-name counterpart of Danvy and Filinski's shift-reset calculus. This "duality" is expressed in the lambda-mu-tp-hat-calculus which is lambda-mu-calculus equipped with a single dynamically-bound continuation variable denoting a resettable toplevel. An equational correspondence having already been proved in A type-theoretic foundation of delimited continuations for call-by-value lambda-mu-tp-hat and Danvy and Filinski's calculus, we simply show here the equivalence between call-by-name lambda-mu-tp-hat and de Groote's calculus. We continue with a comparative study of the operational semantics, continuation-passing-style semantics, and simple typing of both call-by-name and call-by-value versions. Finally, we show the existence of two other canonical calculus of delimited continuations. The first one morally forms an equational correspondance with Sabry's shift/lazy-reset calculus while the second one is a "lazy" version of de Groote's calculus.

Abstract: We investigate the differences between Felleisen et al.'s lambda-C-calculus and Parigot's lambda-mu-calculus (presented, for ease of comparison, with a C-like operator, and extended for expressivity, with a toplevel continuation), in their untyped call-by-value variant. Especially, we show that Parigot's structural substitution of evaluation contexts behaves better in many respects than Felleisen et al.'s substitution of reified evaluation contexts. Still, both calculi are operationally equivalent.

Abstract: We consider a theory of Sigma-types (i.e. a type theory restricted to strong existential -- sometimes also referred to as strong sum). We show that the quantification domain of the Sigma-types is degenerated (i.e. it is provably reduced to at most one element) in presence of computational classical logic, i.e. in presence of a control operator similar to callcc equipped with standard reduction rules. We how however that the non degeneracy is non derivable if the classical operator is typed and the eta-reduction rule specific to this operator (i.e. "callcc_k M -> M, for k not occurring in M") is removed.

Abstract: The paper studies call-by-value Parigot's lambda-mu-calculus (where mu is written with a C operator) extended with a dynamically-scoped continuation variable and shows that the resulting calculus is equivalent to Danvy-Filinski shift-reset calculus. The proof is obtained by decomposing Danvy-Filinski double continuation-passing-style interpretation of shift and reset into a state-passing-style transformation followed by a (single) continuation-passing-style transformation. Different type systems are investigated. They are proved to ensure strong normalisation as soon as, either types are decorated with effects, or reset is used on atomic types only. The paper also justifies the subtraction connective as a relevant construction to simulate in a purely functional way the dynamic aspect of a continuation variable such as the one used to interpret reset. Incidentally, a proof of strong normalisation of classical natural deduction extended with the subtraction connective is given. Note that the journal version also repairs the incorrectly stated Proposition 8 from the conference version.

Abstract: Minimal Classical Logic is defined as the restriction of classical logic which enjoys Peirce's Law but not “ex falso quodlibet” (hence not double negation elimination). Typically, Parigot's lambda-mu-calculus is a denotation for the proofs of minimal classical natural deduction. To get full classical logic, we need to extend lambda-mu-calculus with a constant of type absurd. The computational interpretation of this constant is a toplevel continuation. At the end, we give a refinement of Felleisen et al. C operator which allows for a tight correspondence with lambda-mu-calculus.

Keywords: Call-by-Name, Call-by-Value, Sequent Calculus, CPS-Translations Curry-Howard-de Bruijn Proof-as-Program Correspondence, Duality, Lambda-Calculus.

Abstract: We show that the left-right symmetry of Gentzen sequent calculus relates to a duality between terms and contexts and between call-by-name and call-by-value; we design the lambda-bar-calculus, a variant of lambda-calculus which makes these dualities explicit.

Keywords: Lambda-bar-calculus, Explicit Substitutions, Strong Normalisation, Reducibility

Abstract: We define a notion of reducibility based on sequents instead of formulas. We then give a direct proof of strong normalisation for lambda-bar-calculus with explicit substitution.

Keywords: Game Models, Abstract Machines, Böhm Trees.

Abstract: We show and compare several variants of abstract machines for weak-head reduction in lambda-calculus, PCF, and, more generally, “abstract Böhm trees”. Some of these machines are expressed in a game setting (e.g. the "geometrical abstract machine" which is new). The other ones are expressed as usual environment machine in KAM-style.

Keywords: Game Models, Abstract Machines, Classical Logic, Control Operators, Lambda-mu-calculus.

Abstract: We extend Hyland-Ong game model to PCF with catch and throw. It differs from Ong approach in the sense it weakens the rules while Ong adds new moves. We relate also Lorenzen's E-dialogues, Coquand's notion of debate, Krivine Abstract Machine, Parigot's lambda-mu-calculus and game models.

Keywords: Abstract Machines, Game Models for Computation (Hyland-Ong, Abramsky-Jagadeesan-Malacaria), Geometry of interaction.

Abstract: We show that composition in Hyland-Ong model of PCF is linear head reduction in a call-by-name abstract machine. We show that in Abramsky-Jagadeesan-Malacaria model, it is geometry of interaction. The framework of the paper is pure lambda-calculus, not PCF.

Keywords: Game Semantics of Computation (Hyland-Ong, Abramsky-Jagadeesan-Malacaria).

Abstract: We characterise the Abramsky-Jagadeesan-Malacaria "history-free" strategies in terms of Hyland-Ong innocent strategies (in French).

Keywords: Lambda-calculi with Explicit Substitutions, Confluence, non Strong Termination

Abstract: We show that a simple simply-typed lambda-calculus with explicit substitution and composition but no Map rule is enough to get an infinite computation (in French).

Keywords: Sequent Calculus, Proof/program Correspondence (Curry-Howard Correspondence), Lambda-calculi with Explicit Substitution.

Abstract: We extend the proof as program paradigm to Gentzen's sequent calculus. This is done by defining a variant of lambda-calculus with explicit substitution. This new lambda-calculus, the lambda-bar-calculus provides with a term notation for the sequent calculus proofs.

Keywords: Type Systems, Turing's Completeness, Inconsistent Logical Systems.

Abstract: We show that all partial recursive functions are definable in (logical) Pure Type Systems as soon as they are inconsistent (which is the case of Martin-Löf's system Type:Type, Girard's system U, ...) The proof relies on Friedman's A-translation. As a consequence, type-checking is undecidable in Type:Type.

Keywords: Classical Logic, Cut-Elimination, Program Extracted from Proofs.

Abstract: We define an interleaving game semantics of products.

PhD thesis and dissertations

Keywords: Sequent calculus, Cut-Elimination, Lambda-calculi, Game interpretation of provability (Lorenzen's games and Coquand's games), Classical Logic.

Abstract:

We interpret Gentzen's sequent calculus as a lambda-calculus, hence providing a Curry-Howard correspondence for sequent calculus.

We show that Lorenzen's games are just a paraphrase of provability in a particular sequent calculus

We show that cut-elimination in Coquand's game model corresponds to weak-head cut elimination in the modelled sequent calculus.

Keywords: Formal machine proof, Stratified set theory

Abstract: We formalise Schröder-Bernstein theorem in INRIA's Coq proof assistant (in French).