Nicolas Guenot and Dale Miller spoke at the ChoCola meeting, ENS Lyon on 15 March 2012. The program is available.
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.
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.
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 will be starting this spring on topics related to their Master’s program (MPRI).
- Zakaria Chihani will be working on Proof certificates for some basic proof systems in classical logic. He will be starting 15 March 2012.
- Florence Clerc will be working on Relating double-negation translations and focused proof systems. She will be starting 16 April 2012.