|PROTOCOLLO Home Page||Other Informations|
(Link to Scheduling)
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.
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).
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.
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, ...