Chuck Liang (Prof, Hofstra University, NY, USA) will be visiting the Parsifal team the week of 17 Dec 2012.  He will give the following talk in Salle Philippe Flajolet (2017) of LIX on Wednesday 19 December at 11h.  -Dale

Extending Intuitionistic Logic for Control

From a relatively practical perspective, our goal is to achieve a computationally meaningful interpretation of disjunctive types, including the throwing and catching of exceptions, using a form of non-additive disjunction.  Most of the work on extending the Curry-Howard isomorphism and lambda calculus are based on replacing intuitionistic logic with classical logic.  In such a context “classical implication” is given the same computational interpretation as intuitionistic implication, i.e., as lambda abstraction.  With this interpretation, the body of a lambda term, of *classical* type A->B, may not actually *compute* B in the sense that B is the result of introductions  and eliminations.  Instead, B may be the result of weakening.  This loss of constructivity becomes especially acute in the presense of disjunction: a particular example is found in the classical equivalence between (A->B)vC and (A->C)vB.  This equivalence is not consistent with the concept of localized scope that’s expected in programs.

Our solution to this problem is to introduce a *unified logic* in which classical and intuitionistic logics can co-exist without one subsuming the other.  We introduce “Polarized Intuitionistic Control Logic” (PICL).  This logic is a synthesis of our earliear works PIL and ICL.  In particular, it contains as a natural fragment (ICL) that simply extends intuitionistic logic with an additional logic constant. This simplified fragment is already capable of encoding control operators such as call/cc while preserving intuitionistic implication.  However, for a richer type system, we extend ICL with an additional class of formulas.  We use polarity information encoded in the formulas to control the availability of certain structural rules, which allows us to unify classical and intuitionistic reasoning.  We define a simple but useful Kripke semantics, a tableau/sequent calculus proof system and, most importantly, a natural deduction system with a term calculus.  We also discuss the role of polarization in sequent calculus versus natural deduction systems.

Part of this talk will consist of ongoing work and some non-finalized alternatives will also be discussed.

Florence Clerc was an intern with the Parsifal team during summer 2012.  On Friday, November 30 at 10:00 she will speak at the Deducteam seminar in room Verte 1 at INRIA, 23 avenue d’Italie (metro place d’Italie) on the 5th floor.

Embedding constructiveness into classical logic via double negation translations or polarization
Florence Clerc (INRIA and LIX, Ecole polytechnique)

Abstract: Although originally developed as a tool for proving the consistency of classical logic with respect to constructive reasoning, double negation translations have recently been used to embed classical  reasoning into intuitionistic proofs.  Such translations can then be used to associate constructive functions to classical proofs.  In this paper, we show that if we pick a particular double negation translation from a set of known translations, it is possible to establish an isomorphism between the cut free classical sequent proofs of formula B and the intuitionistic sequent calculus proofs of the translation of B.  In order to get such a strong correspondence of proofs, this isomorphism is constructed between focused sequent proofs in these two logics.  Using the LJF and LKF focused proof systems of Liang & Miller (2009), we can show that focused cut-free classical proofs of a certain polarization of B are isomorphic to a certain double negation translation. In particular, we describe the polarization of classical proofs needed to exactly model the Kuroda translation.

On Nov 23 and 30 François Lamarche is giving a series of two talks at the PPS laboratory, Université Paris VII, as part of the Catégories supérieures, polygraphes et homotopie “Groupe de Travail”.

The title of the series is “Foncteur des chemins dans Cat”.