Computational Interpretations of Proofs
Paris, November 29-30 2007
Small workshop of the
european
TYPES
project & ECO-NET project 16259PG (1)
This workshop is devoted to "computational interpretations
of proofs" in a broad sense: from structural proof theory questions underlying computational interpretations of logics (classical, intuitionistic, modal, etc.)
to concrete program extraction from proofs.
There will be 4 invited talks and the rest of the program will consist of
contributed talks and discussions.
The workshop is open to everyone interested. All proposals of contributed talks
are welcome, including works in progress and discussions of open problems.
If you intend to give a talk or simply participate, please
let us know by sending an
email to cip@pps.jussieu.fr.
See below
the programme and
the location
of the workshop.
Invited Talks:
Contributed Talks:
- René David (University of Savoie, Chambéry, FR) : A direct proof of the confluence of combinatory logic.
- Mauricio Guillermo (University Paris 7, FR): Games on Krivine's classical realisability
- Tom Gundersen (University of Bath, UK): Normalisation via atomic flows
- Vladimir Komendantsky (INRIA Sophia Antipolis, FR): Generic semantics of normalisation in lambda-mu calculus
- Richard McKinley (University of Bern, CH): Herbrand's theorem and cut-elimination
- Paul-André Melliès (University Paris 7, FR): Existential quantification in games and logic
- Mati Pentus (Moscow Lomonossov State University, RU): Simple proof nets for the non-commutative multiplicative linear logic
- Christophe Raffalli (University of Savoie, Chambéry, FR): Programs as Proofs
- Natalia Rubtsova (Moscow Lomonossov State University, RU): Semantics for Justification Logic Corresponding to S5
- Khelifa Saber (University of Savoie, Chambéry, FR): A completeness result for the simply typed lambda-mu-calculus
- Yury Savateev (Moscow Lomonossov State University, RU): The derivability problem for Lambek calculus with one division
- Steffen van Bakel (Imperial College London, UK): Concurrency and classical logic
Participants:
- Lev Beklemishev (Russian Academy of Sciences, Moscow, RU)
- Stefano Berardi (University of Torino, IT)
- Ulrich Berger (University of Wales, Swansea, UK)
- Kai Brünnler (University of Bern, CH)
- Kaustuv Chaudhuri (INRIA Futurs, Palaiseau, FR)
- René David (University of Savoie, Chambéry, FR)
- Daniel de Carvalho (Loria, Nancy, FR)
- Lucas Dixon (University of Edinburgh, UK)
- Mauricio Guillermo (University Paris 7, FR)
- Tom Gundersen (University of Bath, UK)
- Philippe Hesse (University Paris 7, FR)
- Pierre Hyvernat (University of Savoie, Chambéry, FR)
- Delia Kesner (University Paris 7, FR)
- Vladimir Komendantsky (INRIA Sophia Antipolis, FR)
- Jean-Louis Krivine (University Paris 7, FR)
- Olivier Laurent (University Paris 7, FR)
- Pierre Letouzey (University Paris 7, FR)
- Pascal Manoury (University Paris 6, FR)
- Richard McKinley (University of Bern, CH)
- Laurent Méhats (INRIA Futurs, Palaiseau, FR)
- Paul-André Melliès (University Paris 7, FR)
- Dale Miller (INRIA Futurs, Palaiseau, FR)
- Jean-Francois Monin (University Joseph Fourier, Grenoble, FR)
- Vivek Nigam (Ecole Polytechnique, Palaiseau, FR)
- Karim Nour (University of Savoie, Chambéry, FR)
- Mati Pentus (Moscow Lomonossov State University, RU)
- Michel Parigot (University Paris 7, FR)
- Christophe Raffalli (University of Savoie, Chambéry, FR)
- Paul Roziere (University Paris 7, FR)
- Natalia Rubtsova (Moscow Lomonossov State University, RU)
- Khelifa Saber (University of Savoie, Chambéry, FR)
- Yury Savateev (Moscow Lomonossov State University, RU)
- Samanta Socci (University of Siena, IT)
- Lutz Strassburger (INRIA Futurs, Palaiseau, FR)
- Aldo Ursini (University of Siena, IT)
- Silvia Vecchiato (University of Siena, IT)
- Steffen van Bakel (Imperial College London, UK)
Programme:
Thursday, November 29
Friday, November 30
Location of the Workshop:
175, rue Chevaleret, 75013 PARIS France
The nearest metro station is "Chevaleret" (line 6). To get to
the building see
map
Organization:
Abstracts:
- Lev Beklemishev (Moscow): Proof interpretations of modal logic
Abstract: We shall discuss two different interpretations of modal logic related to proofs, in particular, the provability logic and Artemov's logic of proofs LP. The two interpretations, although related to each other, are motivated by different kind of concerns and present different possibilities for applications. We shall survey some relationships of LP with constructive logic and with epistemic logic and discuss various open questions in this area.
- Stefano Berardi (Torino) : A computational interpretation of classical proofs through parallel computations
Abstract: We argue in favor of the following thesis: there is an intric link between the computation we can unwing from classical proofs and parallel computations. We introduce a model for computations extracted from classical proofs based on parallel computations and on the concept of learning in the limit. The aim of our research is designing parallel extensions of the existing continuation languages.
- René David (Chambéry) : A direct proof of the confluence of combinatory logic.
Abstract: n the proofs as programs paradigm, Combinatory Logic is the program counterpart of proofs in Hilbert style systems. It has the same properties as the Lambda Calculus : confluence, strong normalization of typed terms, ... Unlike in Lambda calculus, there is no use of bounded variables and this should make reasonning on it simpler. However, all known proofs of confluence use the confluence of the Lambda Calculus and thus Combinatory Logic is not a self contained theory. The question of finding a direct proof has been stated long ago by R Hindley and is the first one in the TLCA list of open problems (http://tlca.di.unito.it/opltlca/). I give here such a proof.
- Ulrich Berger (Swansea) : Programs from proofs in analysis.
Abstract: In the first part of the talk I give an overview of the work on program extraction from proofs in analysis by the Minlog group in Munich and Swansea. Then I describe a very recent approach based on an inductive/coinductive characterisation of uniform continuity that can be used to extract memoized programs for uniformly continuous real functions.
- Jean-Louis Krivine (Paris) : Games on valid formulas and network protocols
Abstract: I will describe a remarkable relation between the games on valid formulas of predicate calculus (or, more generally, on \Pi_1^1 true formulas) and the specification of network protocols. Some simple examples will be given, such as the acknowledgement of one or several packets or the "3-ways handshake" (initialisation of a TCP session).
There is a paper, with Y. Legrandgerard, at http://www.pps.jussieu.fr/~krivine/articles/Network_eng.pdf
- Mauricio Guillermo (Paris): Games on Krivine's classical realisability
Abstract: J. L. Krivine proposed a game's interpretation for first order formulae in prenex normal form and relativized to the integers. By means of this interpretation, a term realizing a formula implements a winning strategy for the associated game. More recently, in "Realisability: A machine for analysis", he proposed a game's semantics for first order formulae which preserves the fact that a term realizing a formula implements a winning strategy for its associated game. This game's semantics allows to characterise by a formula, the specification of an interactive program. In this talk we will present a variant of the last krivine's definition of games and, depending on time, we will explain some examples about specification.
- Tom Gundersen (Bath): Normalisation via atomic flows
Abstract: We introduce diagrams, called "atomic flows", that represent the causual relation between atoms in derivations. A new notion of normalisation, which generalises cut-elimination, is then defined in terms of atomic flows, and a normalisation procedure presented. This is work in progress, where one of the aims is to investigate computational interpretations of this normalisation procedure.
- Vladimir Komendantsky (Sophia Antipolis): Generic semantics of normalisation in lambda-mu calculus
Abstract: We give a semantical account of _normalisation by evaluation_ in the simply typed lambda-mu calculus. It amounts to a generic categorical construction which can be applied to various models of the lambda-mu calculus (domain-theoretic, etc.) to obtain concrete examples. We describe the case of the call-by-name continuation passing style translation; hence the semantics that we present is call-by-name. At the level of the propositions-as-types correspondence, this yields a constructive semantics of _normalisation_ of classical proofs modulo a double negation translation.
- Richard McKinley (Bern): Herbrand's theorem and cut-elimination
Abstract: I will introduce an abstact proof system for first-order classical logic (Herbrand expansion proofs), which simultaneously give an elegent statement of Herbrand's theorem and are proofnet-like objects for first-order classical logic. Additionally, there is a notion of cut for these objects, and a strongly normalizing cut-elimination algorithm, about which I will sketch some details.
- Paul-André Melliès (Paris): Existential quantification in games and logic
Abstract: In this tutorial talk, I will explain how to see proofs as purely combinatorial objects, generated by algebraic principles. This point of view clarifies the status of game semantics in logic, and opens fascinating connections to mathematical physics (knot theory, quantum algebra, etc.) I will also indicate how to incorporate quantification in the picture, starting from Hyland's formulation of Goedel's Dialectica translation, and Krivine's realizability model of Second Order Peano Arithmetic.
- Mati Pentus (Moscow): Simple proof nets for the non-commutative multiplicative linear logic
Abstract: In linear logic, proof nets are used for representing derivations in an intuitive and redundancy-free way. We consider the non-commutative multiplicative linear logic. Given a formula (or a sequent), the variable part in proof search consists of axiom links. We discuss a notion of proof net, which provides an efficient algorithm for checking whether given axiom links yield a proof net.
- Christophe Raffalli (Chambéry): Programs as Proofs
Abstract: We will present what a proof in PML is (or will be soon: a first version of the proof system is almost implemented). The concept is quite general and could apply to most functional languages with exceptions (the presence of exceptions is required !). The main tool will be a kind a Knuth-Bendix algorithm to get contradiction from hypothesese of the shape "t reduces to v" where "t" is a term of the language and "v" is a value.
- Natalia Rubtsova (Moscow): Semantics for Justification Logic Corresponding to S5
Abstract: We introduce a logic of evidence-based knowledge \mbox{\sf S5}_{\sf n}\mbox{\sf LP(S5)}. It is a multi-agent logic of knowledge enriched by evidence assertions of the form $t\!:\!\varphi$ where $t$ is an {\it evidence term}. The! knowledge of an agent is axiomatized by the modal logic \mbox{\sf S5}. The evidence-based knowledge operator is described by the logic of proofs $\mbox{\sf LP(S5)}$, which is also based on \mbox{\sf S5}. The resulting systems \mbox{\sf S5}_{\sf n}\mbox{\sf LP(S5)} are provided with Kripke-style semantics. The corresponding completeness theorems are proven.
- Khelifa Saber (Chambéry): A completeness result for the simply typed lambda-mu-calculus
Abstract: We define a semantic of realisability for the simply typed lambda-mu-calculus. This semantic allows us to provide a proof of the strong normalization theorem of the calculus via the adequation lemma, which stipulates that: each typed term is in the interpretation of its type. In our talk we are interested by the converse of this lemma, i.e. "can we find a class of types for which the converse of the correcteness lemma holds?". We dealt with this problem and prove a completeness result for the simply typed lambda-mu-calculus
- Yury Savateev (Moscow): The derivability problem for Lambek calculus with one division
Abstract: We prove that the derivability problem for Lambek calculus with one division is decidable in polynomial time and present an algorithm for it.
- Steffen van Bakel (London): Concurrency and classical logic
Abstract: We study the pi-calculus, where the family of names is enriched with pairing, and define a notion of type assignment that uses the type constructor arrow. We encode the circuits of the calculus X into this variant of pi, and show that reduction and type assignment are preserved. Since X enjoys the Curry-Howard isomorphism for Gentzen's
calculus LK, this implies that all proofs in LK have an encoding in pi. We then enrich the logic with the connectors And, Or and Negation, and show that also these can be represented in pi.
(1) ECO-NET project 16259PG is a project on "computational interpretations of modal logics" gathering together teams from Paris, Moscow and Tbilisi.