- 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.
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
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.
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.
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.
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).
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.