Stefan Hetzl, currently at the Vienna University of Technology, will be joining the Parsifal team for a three month postdoc during the dates 01/07/2012 and 30/09/2012. He will be working with (at least) Chaudhuri and Miller on the general problem of canonicity in classical sequent calculus.

May 05

## Beniamino Accatoli speaks at Rocquencourt

I N R I A – Rocquencourt

Amphi Turing du bātiment 1

Lundi 7 mai, 10h30

Beniamino Accatoli

LIX

Abella formalization of lambda-calculus residual theory

Abella is a new proof assistant developed by Andrew Gacek and based on work of Gacek, Miller and Nadathur. Its main feature is a primitive handling of binders via higher order abstract syntax and the nabla quantifier. In the talk we introduce the system and present a formalization of the residual theory of lambda calculus. This development is actually a re-formalization of a work of Huet in Coq. Thanks to the features of Abella and to a re-understanding of the Huet’s work we get an elegant and extremely concise formalization of the cube lemma for residuals. We also discuss some work in progress towards the formalization of more advanced results.

Apr 25

## Talk by Maribel Fernandez, 26 April

**Nominal Completion for Rewrite Systems with Binders**

*Maribel Fernandez*. Joint work with Albert Rubio.

Apr 19

## Two talks for Friday, 4 May 2012

We will have two talks on Friday, 4 May 2012. Pierre-Louis Curien will speak at 11h and Chuck Liang will speak at 14h30. Both talks will be in the Salle de Reunion of LIX.

*System L syntax for sequent calculus*

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. Slides are available at http://www.pps.jussieu.fr/~

*From Intuitionistic Logic to Polarized Intuitionistic Logic: Double Negation, Polarization, Focalization, and Semantics*

Apr 11

## Workshop on “Cross Perspectives on Proof Systems and their significance”

There will be a workshop titled “Cross Perspectives on Proof Systems and their significance” on May 3, 2012 at ENS, 45 rue d’Ulm 75005 Paris. Miller will be one of the speakers. The program is available.

Apr 05

## Celebration of the career of Peter Andrews

On 4 April 2012, there was a reception for Peter Andrews on the ocassion of his retirement from the Mathematics Department at Carnegie Mellon University. Dale Miller offered some personal words and some scientific talks were presented the following day.

Mar 30

## CFP: CPP 2012 – 2nd International Conference on Certified Programs and Proofs

The Second International Conference on Certified Programs and Proofs (CPP 2012) will be held in Kyoto, Japan during December 13-15, 2012. It will be co-located with APLAS 2012.

CPP is a new international forum on theoretical and practical topics in all areas, including computer science, mathematics and education, that consider certification as a essential paradigm for their work.

Chris Hawblitzel (Microsoft Research Redmond) and Dale Miller (INRIA Saclay and LIX, Ecole Polytechnique) are the co-PC chairs.

Mar 29

## ASL special session on Structural Proof Theory and Computing

During the 2012 ASL annual meeting in Madison Wisconsin, there will be a special session on Structural Proof Theory and Computing that has been organized by Dale Miller. Several members and former members of Parsifal will present their research work during this annual meeting of the Association for Symbolic Logic.

The study of the structural properties of proofs has evolved a great deal since Gentzen’s original proof of cut-elimination for classical and intuitionistic sequent calculus proofs. The recent 20-30 years has seen an explosion of results in the area of Structural Proof Theory that have brought us linear logic and a wide range of applications to computer science. This special session will focus on recent work on structural proof theory that has applications in computing and for which computing has been, in part, an important motivation.

The official program for the full conference can be found here. This session includes the following speakers.

- Dale Miller, An overview of Structural Proof Theory and Computing
- Alexis Saurin, Proof search and the logic of interaction
- David Baelde, A proof theoretical journey from programming to model checking and theorem proving
- Stefan Hetzl, Which proofs can be computed by cut-elimination?
- Marco Gaboardi, Light Logics for Polynomial Time Computations

Mar 19

## Chuck Liang speaks at GdT Théorie des types et réalisabilité

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.

Mar 16

## Intern starts today

Zakaria Chihani is starting his M2 level internship at LIX on the topic of Proof certificates for some basic proof systems in classical logic.