Two talks will be given at the GdT Théorie des types et réalisabilité in the salle orange au 5e étage, 23 avenue d’Italie.
Mercredi 21 mars, 14h and 15h15, salle orange 1 (double séance)
Chuck Liang
An Intuitionistic Logic for Sequential Control
We introduce the propositional logic ICL for “Intuitionistic Control Logic”, which adds to intuitionistic logic elements of classical reasoning without collapsing it into classical logic. As in linear logic, ICL contains two constants for false. However, the semantics of this logic is based on those of intuitionistic logic. Kripke models are defined for this logic, which are then translated into algebraic and categorical representations. In each case the semantics fit inside intuitionistic frameworks (Heyting algebras and cartesian closed categories). We define a sequent calculus and prove cut-elimination. We then formulate a natural deduction proof system with a variation on the lambda-mu calculus that gives a direct, computational interpretation of contraction. This system satisfies the expected properties of confluence and strong normalization. It shows that ICL is fully capable of typing programming language control constructs such as call/cc while maintaining intuitionistic implication as a genuine connective. We then propose to give a more computationally meaningful interpretation of disjunction in this system.
Pierre-Louis Curien
System L syntax for sequent calculi
We recall two related syntaxes for focalised logic (linear and classical), derived from Curien-Herbelin’s duality of computation work, that have been proposed by Munch-Maccagnoni in 2009 and (for the classical case) by Curien – Munch-Maccagnoni in 2010. We explain how the latter (with explicit “shifts”, i.e. change-of-polarity operators) is an “indirect style” version of the former. We explain their relation with tensor logic and LLP.
We then discuss bilateral systems, in which the duality positive/negative is made distinct from the duality programme/context. We recover (a sequent calculus version of) Levy’s Call-By-Push-Value as a fragment, and we discuss the conditions under which the shifts are or are not forced to define the monad of continuations. This last part is developped in collaboration with Marcelo Fiore.
