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