Guenot and Miller speak at ChoCola, Lyon

Nicolas Guenot and Dale Miller spoke at the ChoCola meeting, ENS Lyon on 15 March 2012.  The program is available.

Chuck Liang speaks 20 March 14h

The following talk will be held in the Salle de Conference of LIX at 14h on 20 March 2012.

An Intuitionistic Logic for Sequential Control

by Chuck Liang

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.

Workshop on Certificates and Computation

An informal workshop will take place at ITU (Copenhagen) during March 12-13, on the general topic of certificates. Although most talks will be about proof theory and logical frameworks, we seek to have discussions on the more general notion of certificate, notably in complex security contexts such as e-voting. Several people from Parsifal will attend and give talks.


Chuck Liang visits Parsifal in March-April

Prof. Chuck Liang of Hofstra University, USA, spends part of his sabbatical in the Parsifal team in March and April. He will arrive in Paris on 5 March.

Brigitte Pientka visits Parsifal / Funding success

Prof. Brigitte Pientka of McGill University, Canada, visits Parsifal and LIX during 21 – 24 February. She will give a talk on her POPL 2012 paper, “Programming with Binders and Indexed Data-types“.

In related news, the PSR-SIIRI project “Promis: de la théorie des preuves à la pratique de la démonstration automatique” with Prof. Pientka and Dale Miller as PIs was just accepted by the Canadian government and will be funded for the maximum amount of 150,000 CAD for three years. Other collaborators on this project include Prof. Frank Pfenning of Carnegie Mellon University and Prof. Gopalan Nadathur of the University of Minnesota, USA.

Two new interns for Spring/Summer 2012

Two new interns will be starting this spring on topics related to their Master’s program (MPRI).

Book to be published by Cambridge University Press

The book Programming with higher-order logic by Dale Miller and Gopalan Nadathur will be published by Cambridge University Press by the end of May 2012.  It is available for pre-ordering on and  The table of contents is available.
Book cover

Paper accepted to QAPL 2012

The following paper was accepted to QAPL 2012: A non-local method for robustness analysis of floating point programs by Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. Draft dated 3 Feb 2012 (HAL).

New site

Welcome to the new Parsifal web-site. Not everything from the old site has been transferred over yet, but the key bits are in place.