Dale MILLER

Author's posts

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.  

ProofCert funded PostDoc positions available

One or two ProofCert-funded postdoc positions are available within the Parsifal team.

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, …

Continue reading

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 …

Continue reading

A talk by Thanos Tsouanas

Our visitor Thanos will speak Tuesday (22 Jan) at 14h in Salle Marcel-Paul Schützenberger. Game semantics for disjunctive logic programming by Thanos Tsouanas Denotational semantics of logic programming and its extensions (by allowing negation, disjunctions, or both) have been thoroughly studied.  In 1998, a game semantics was given to definite logic programs by Di Cosmo, Loddo, …

Continue reading

Thanos Tsouanas visits for two weeks

We have a visitor to the team during the next two weeks.   Thanos Tsouanas http://perso.ens-lyon.fr/thanos.tsouanas/ is doing his PhD at ENS Lyon with Olivier Laurent.  Part of his PhD (via a Marie Curie fellowship)  requires him to undertake a “secondment” at a school outside ENS Lyon.  Thus his visit here.

Chuck Liang speaks at 19 Dec at 11h

Chuck Liang (Prof, Hofstra University, NY, USA) will be visiting the Parsifal team the week of 17 Dec 2012.  He will give the following talk in Salle Philippe Flajolet (2017) of LIX on Wednesday 19 December at 11h.  -Dale Extending Intuitionistic Logic for Control From a relatively practical perspective, our goal is to achieve a …

Continue reading

An internship proposed

Dale Miller is proposing an internship for the spring/summer of 2013: Moving focusing proof systems to arithmetic.  

Florence Clerc speaks at INRIA-Paris

Florence Clerc was an intern with the Parsifal team during summer 2012.  On Friday, November 30 at 10:00 she will speak at the Deducteam seminar in room Verte 1 at INRIA, 23 avenue d’Italie (metro place d’Italie) on the 5th floor. Embedding constructiveness into classical logic via double negation translations or polarization Florence Clerc (INRIA and LIX, …

Continue reading

Lamarche speaks on “Foncteur des chemins dans Cat”

On Nov 23 and 30 François Lamarche is giving a series of two talks at the PPS laboratory, Université Paris VII, as part of the Catégories supérieures, polygraphes et homotopie “Groupe de Travail”. The title of the series is “Foncteur des chemins dans Cat”.