Olivier Savary-Bélanger joins us for a three month internship starting May 13. He will be working on automating various aspects of context relations in Abella, as part of the RAPT project.
Apr 20
Stefan Hetzl gets a new position in Vienna
Stefan Hetzl (former postdoc in Parsifal) has recently won a sponsorship from the Vienna Science Technology Fund that will allow him to build a new research team at the Technical University of Vienna. For more about this 1.5 million euro award, read the press releases in English and German.
Apr 19
Nicolas Guenot successfully defends his Ph.D.
Nicolas Guenot (new web page) defended his Ph.D. on 10 April at LIX under the supervision of Lutz Straßburger. He will continue to a postdoctoral position at Demtech at the IT University, Copenhagen.
Mar 25
Paper accepted to LICS 2013
The submission to LICS 2013 titled Unifying Classical and Intuitionistic Logics for Computational Control by Chuck Liang and Dale Miller was accepted. The final draft of this paper is due 26 April. If you have any comments on the earlier draft, please get them to one of the authors by then.
Mar 24
Jean Pichon starts as an intern
Jean Pichon started his M2 internship via MPRI within the team on 18 March. He will be here until late August. The proposal for his internship is available.
Mar 24
Paper accepted to CADE 2013
The submission to CADE 2013 titled Foundational proof certificates in first-order logic by Zakaria Chihani, Dale Miller, and Fabien Renaud was accepted. The final draft of this paper is due 1 April. If you have any comments on the earlier draft, please get them to one of the authors by then.
Mar 14
ProofCert funded PostDoc positions available
One or two ProofCert-funded postdoc positions are available within the Parsifal team.
Feb 26
Talk by Danko Ilik, 19 March 2013
Control operators as constructive extensions of intuitionistic logic
Speaker: Danko Ilik
Venue: Salle Philippe Flajolet, LIX, Alan Turing Building
Date: 19 March 2013, 13h30
Since the observations of Felleisen and Griffin, in the early 1990s,
that control operators from the theory of programming languages can be
used to extend the Curry-Howard correspondence from intuitionistic to
classical logic, these operators (and, by extrapolation, computational
side-effects) have been taught of as non-constructive. Yet, in recent
works of Herbelin and the author, it has been shown that constructive
logical systems, weaker than classical logic, and stronger than
intuitionistic logic, can be built using them.
In this talk, I will survey these systems and discuss some of their
recent applications and meta-mathematical implications, like the
provability of Open Induction on Cantor space, or the status of the
arithmetical Church’s Thesis.
Feb 18
Small Workshop on Formal Meta-Theory, 5-6 March
Parsifal will organize a workshop on formal meta-theory during 5-6 March to coincide with the visit of Prof. Brigitte Pientka from McGill during that week. We will also welcome some additional visitors from McGill: Andrew Cave, Francisco Ferreira, Olivier Savary-Bélanger, and David Thibodeau.
Feb 11
A talk by Zena Ariola
Zena Ariola (Professor from the University of Oregon) is currently visiting PPS in Paris. She will visit LIX and give the following talk.
Call-by-need: reduction, continuation passing style and abstract machine
by Zena Ariola
27 Feb 2013, 11h, Salle Philippe Flajolet, Alan Turing Building
INRIA-Saclay & LIX, Ecole Polytechinque
We introduce the call-by-need calculus and discuss how it represents Wadsworth’s graph reduction. We will then present a continuation-passing style (CPS) transformation which brings to light the fact that call-by-need variables are not given meaning by substitution. We relate this CPS to the pi-calculus. We follow with the classical extension which raises issues regarding the sharing of bindings. Two approaches will be discussed, one inspired by natural deduction and the other by the sequent calculus. One example will show how the two semantics differ.
