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
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 prove termination of nominal rewriting rules,
generalising the recursive path ordering to take into account
alpha equivalence. Using this ordering, we have designed a
Knuth-Bendix style completion procedure (to our knowledge,
this is the first completion procedure available for rewriting
systems with binders). An implementation can be found at
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
From Intuitionistic Logic to Polarized Intuitionistic Logic: Double Negation, Polarization, Focalization, and Semantics
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/~
We develop a system called Polarized Intuitionistic Logic (PIL). This logic predates, and is similar to the logic “ICL,” which was the subject of other talks. However, while ICL has more of the characteristics of an intermediate logic with a natural deduction and term calculus, the goal of PIL is to *combine* classical logic and intuitionistic logic into a single system, both semantically and proof-theoretically. We begin by describing a double-negation translation of classical logic into intuitionistic logic, then assign polarities to the translated formulas. We then use an intuitionistic, focused sequent calculus to show that the translations of the classical connectives observe focalization, which is to say that they are valid as synthetic connectives. The sequent calculus we derive merges LJ and a version of LC, in which classical proofs also have access to a *stoup*. This combination is much more than a disjoint union: classical and intuitionistic connectives can freely mix without either destroying the other. Kripke and algebraic semantics are also defined for this logic.Note: this logic was the subject of an earlier talk given in June 2011. However, a totally different approach is used to describe the logic and there will also be much material that is entirely new.
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.
