Nominal Completion for Rewrite Systems with Binders Talk by Maribel Fernandez. Joint work with Albert Rubio. Venue: Salle de reunion, 10h30 Thursday 26 April 2012 Nominal rewriting generalises first-order rewriting by providing support for the specification of binding operators, using the nominal approach. In this talk, I will present a new ordering that can be used to …
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 Pierre-Louis Curien We recall two related syntaxes for focalised logic (linear and classical), derived from Curien-Herbelin’s …
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.
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.
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 …
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 …
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 …
Zakaria Chihani is starting his M2 level internship at LIX on the topic of Proof certificates for some basic proof systems in classical logic.
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 …