PROTOCOLLO Home Page

Other Informations

General Presentation of the Track-Meeting on Semantics

The meeting on "Semantics" will take place on Friday 17th (14:30-18:30)
and Saturday 18th (9:30-12:30 e 14:00-17:00).
The idea is to bring together researchers involved in the italian
national project “Protocollo”, one of whose research mainstreams is
about semantics.
The meeting is intended to be a very informal one. There will be 4
invited speakers, who will present stable material and ideas, which
should be the basis of the discussions.
The three main themes will be:
- differential proof-nets
- denotational semantics of "light" logics
- the question of injectivity (or "semantic separation").

Invited Speaker:	Program  (Link to Scheduling)
Patrick Baillot	TITLE:Stratified coherence spaces: a denotational semantics for Light Linear Logic. ABSTRACT: Light linear logic (Girard95) is a variant of linear logic which admits a polynomial time cut-elimination procedure and provides a proofs-as-programs approach to polynomial time computation . In this work we present a semantical analysis of LLL: a variant of coherence spaces   is introduced and we prove that it is a sound model for this system,   but not for usual linear logic. A simpler version of the model   yields a sound semantics of Elementary linear logic, which is the   analog of LLL for the class of Kalmar elementary functions.
Pierre Boudes	TITLE:MELLpol, Designs (Games) and the Relational Model ABSTRACT: We give a synthetic representation of polarized proof nets for multiplicative exponential linear logic with polarities and without atoms. In the spirit of the connection between Games and Girard's Ludics enlighted by Faggian and Hyland, a strategy interpreting a polarized proof net in Laurent's Games can be represented by a finite tree, a "design" in Ludics. In this talk, we present directly the interpretation of proof nets by designs. As for Laurent's Games, this interpretation is full and faithfull. We then show how this synthetic representation of proofs carries their interpretations in the relational model. We further investigate the injectivity (faithfullness) issue of the relational model in that setting, and we also show a peculiar model derived from coherent spaces which is fully complete for affine multiplicative linear logic with polarities (MELLpol without contractions).
Thomas Ehrhard	TITLE:Differential nets and uniformity ABSTRACT: I will introduce an extension of linear logic proof-nets corresponding to the differential lambda-calculus and explain how ordinary lambda-terms can be completely Taylor-expanded in a corresponding extension of the lambda-calculus similar to Boudol's resource lambda-calculus. The resource terms obtained in that way are "uniform" and behave particularly well with respect to reduction.
Olivier Laurent	TITLE: Between polarized proof-nets and polarized games: injectivity, ... ABSTRACT:  We study the relation between a "syntactical object": sliced polarized proof-nets and a "semantical object": polarized games. We show that syntax is abstract enough and semantics is precise enough to get a "coincidence"  between them (namely a categorical equivalence). In a first step, we will describe the interpretation of proof-nets in games showing that it gives a model of cut-elimination (and expansion of axioms). In a second step, we will focus on the much more stronger properties of this interpretation: injectivity, surjectivity, ...