Oct 19

Daniel Weller visits and speaks 23-24 Oct 2012

Daniel Weller from the Vienna University of Technology will give a talk on 23 October.  He will be visiting Tuesday afternoon and Wednesday.  If you would like to meet with him, please send email to Dale.
Considering Proofs As Services
Daniel Weller,  Vienna University of Technology
Tuesday, 23 Oct 2012, 15h, Saclay Salle Flajolet
In this talk, we present a planned project that will investigate particular uses of formal proofs that have, as far as I am aware, not been considered yet. We take the notion of “software as a service”, in which the result of the execution of code on some data is provided to a user (instead of the code itself), and consider how formal proofs can be used in such a situation. For example, if the code has a correctness proof, it can be used to construct a correctness proof of the result of the execution. If done naively, this proof contains the full correctness proof of the code. This naturally leads to the problem of elimination of information from a proof, which can be accomplished by cut-elimination.
One way to analyse this situation is to focus on the “non-propositional”, i.e. first- and higher-order, content of a proof. If time permits, in the second part of the talk we sketch an approach to the analysis of cut-elimination from that point of view by applying methods from the epsilon-calculus (due to David Hilbert) to expansion tree proofs (due to Dale Miller).

Oct 14

RAPT/Promis Workshop in McGill University, Canada

Several members of Parsifal will participate in the Promis workshop in McGill University in Canada during 17–18 October, funded in part by the Equipe Associée RAPT. Abstracts of the talks are already available, and slides will be posted as they become available.

Oct 09

David Baelde visits and speaks

David Baelde (MdC, LSV, Cachen) will visit the team on Friday 12 Oct 2012.  A schedule of his visit is below.
  • 10h30 – noon   informal discussions focusing on, say, Abella related topics.
  • noon-14h         lunch
  • 14h-15h30       talk by David.  Title and abstract below.
  • 15h30-17h       informal discussions focusing on, say, Bedwyr related topics.
Hopefully we get to speak about various proof theory topics as well during the day.  If you want to meet with David about specific things, please let him and I know.
Title: Fixed points, definitions, and parity
I will talk about various proof formalisms dealing with (co)inductive specifications. At the level of formulas, we’ll have definitions on one hand, and fixed point combinators on the other; at the level of proofs, we’ll have (co)induction rules, but also infinite and cyclic proofs that only unfold definitions. These different styles are intuitively related, but I’ve been missing formal results for a long time. I’ll present such formal relationship by bringing in mu-calculus and parity games, showing that they make a lot of sense in sequent calculus, though hard questions remain.

Oct 08

New paper on Combining Intuitionistic and Classical Logics

The following paper has recently been accepted and published by the Annals of Pure and Applied Logic.

Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic,
by Chuck Liang and Dale Miller.

Available online from http://dx.doi.org/10.1016/j.apal.2012.09.005 and
http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/pil-final.pdf .

Oct 02

Matteo Cimini joins as a Post Doc

Matteo Cimini, a recent PhD student from the Computer Science Department at Reykjavik University in Iceland, joined Parsifal as a postdoc for 12 months starting 1 October 2012.

Sep 17

Daniel Seidel speaks 20/09 at 13h30

From Lutz Strassburger:

I’d like to announce a talk by Daniel Seidel (University of Bonn, Germany) on
   “Free Theorems in Languages with Real-World Programming Features”
The talk takes place this Thursday 20/09 at 13:30 in the Prefab meeting room.

Abstract:  Free theorems, type-based assertions about functions, have become a prominent reasoning tool in functional programming languages. For example, they are employed to validate program transformations. But their correct application requires a lot of care. Restrictions arise due to features present in a real-world programming language, but not in the language free theorems were originally investigated in.

We give a short introduction to the theory of free theorems and consider restrictions that arise due to general recursion and forced strict evaluation, as present in the functional programming language Haskell.

In particular, we consider a counterexample generator that tells if and why restrictions on a certain free theorem arise due to general recursion. If a restriction is necessary, the generator, that relies on a proof search algorithm for intutionistic logic and a refined type system for our language, provides a counterexample to the unrestricted free theorem. Thus, we may on the one hand boost the understanding of restrictions and on the other hand hint to cases where restrictions are superfluous.

Concerning restrictions that arise due to forced strict evaluation, we present a refined type system that allows to localize the impact of forced strict evaluation. Refined typing results in stronger free theorems and therefore raises the value of the theorems.

As formal ground for our investigations, we employ different lambda calculi equipped with a denotational semantics.

Sep 05

Lectures from the Paraty Proof Theory School

Elaine Pimentel just sent me some information about the Proof Theory School at Paraty, Brazil (August 27 – September 1, 2012). Topics related to Linear Logic, Ludics, and the Geometry of Interaction were presented. The pdf files of the lecture material are available.

Sep 05

Some changes in the team’s postdocs

Beniamino Accattoli has finished his postdoc at Parsifal and has now moved to Pittsburgh (USA) to start a postdoc at Carnegie Mellon University.

Fabien Renaud is starting a year-long postdoc with Parsifal (funded by ProofCert) this week. He will take an office in the prefab until our move to the new building.

Stefan Hetzl has accepted a year-long postdoc funded by the ANR Structural grant starting 1 October 2012 (he is funded by a different postdoc until then).

Aug 30

Accepted papers for CPP 2012

The list of accepted papers for CPP 2012 can be found here.  The team will have two papers at this conference.

  1. Kaustuv Chaudhuri. Compact Proof Certificates for Linear Logic.
  2. Beniamino Accattoli. Proof pearl: Abella formalization of lambda calculus cube property.

Aug 20

Workshop dates: 15 & 16 Nov 2012

The Parisfial team is planning to host a meeting in the Alan Turing building (on the Polytechnique campus) on 15 and 16 November 2012 between us and our colleagues from Vienna.  We hope to involve colleagues also from Innsbruck and PPS (Paris).   Save the date.

Local organizers:  Kaustuv Chaudhuri and Stefan Hetzl.