PROTOCOLLO Home Page | Other Informations |

General Presentation of the Track-Meeting on Semantics

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 ModelABSTRACT: 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 uniformityABSTRACT: 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 syntaxis 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, ... |