Nicolas Guenot and Dale Miller spoke at the ChoCola meeting, ENS Lyon on 15 March 2012. The program is available.
Mar 15
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.
Mar 06
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.
Feb 17
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.
Feb 17
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.
Feb 14
Two new interns for Spring/Summer 2012
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.
Feb 08
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 Amazon.com and Amazon.fr. The table of contents is available.
Feb 08