PROTOCOLLO Home Page Other Workshop Informations
       
Scheduling

Wednesday  15th September
(Aula Magna del Rettorato -- Via Verdi 8)
09:30 -- 10:00
Opening -- Simona Ronchi Della Rocca (project  leader)
10:00 -- 11:00
J.-Y. Girard (invited speaker)
11:00 -- 11:30
Coffee-Break
11:30 -- 12:15
S. Guerrini (track presentation of proof theory)
12:15 -- 14:30
Lunch
14:30 -- 15:30
M. Hyland (invited speaker)
15:30 -- 16:15
L. Roversi (track presentation of computational complexity)
16:15 -- 16:45
Coffee-Break
16:45 -- 17:45
J. Vauzeilles (invited speaker)
17:45 -- 18:30
L. Tortora De Falco (track presentation of semantics)


Thursday 16th September
(Aula Magna di Biologia - Ex Caserma Podgora
             -- Via Accademia Albertina 13)
09:30 -- 10:00
V. M. Abrusci
10:00 -- 10:30
S. Guerrini (a joint work with A.Masini)
10:30 -- 11:00
C. Faggian (a joint work with F.Maurel)
11:00 -- 11:30
Coffe-Break
11:30 -- 12:00
G. Bellin
12:00 -- 12:30
A. Fleury
12:30 -- 13:00
E. Pimentel (a joint work with S.Ronchi and L.Roversi)
13:00 -- 15:00
Lunch
15:00 -- 15:30
U. Dal Lago
15:30 -- 16:00  L. Roversi
16:00 -- 16:30
Coffe-Break
16:30 -- 17:30
M. Pedicini  (a joint work with F.Quaglia) + DEMO
20:30
Social dinner



Friday 17th September
(Aula Magna di Biologia - Ex Caserma Podgora
             -- Via Accademia Albertina 13)
09:30 -- 10:00
P. Di Gianantonio
10:00 -- 10:30
M. Pagani
10:30 -- 11:00
L. Paolini (joint work with E. Pimentel and S.Ronchi)
11:00 -- 11:30
Coffee-Break
11:30 -- 12:50
Business meeting
12:50 -- 13:00
Closure
13:00 -- 14:30
Lunch
 
  Start Track-Meeting on Semantics

The scheduling will be decided during the meeting, and the following is
just a proposal (containing short abstracts on stable subjects).
14:30 -- 15:30 Thomas Ehrhard 
15:30 -- 16:30 Discussion and Coffe Break
16:30 -- 17:30 Patrick Baillot
17:30 -- 18:30 Discussion




Saturday 18th September
(Dipartimento di Informatica
             -- C.so Svizzera 185)

Track-Meeting on Semantics

The scheduling will be decided during the meeting, and the following is
just a proposal (containing short abstracts on stable subjects).
09:30 -- 10:30
Olivier Laurent
10:30 -- 11:30
Discussion
11:30 -- 12:30
Pierre Boudes 
12:30 -- 14:30
Lunch
14:30 -- 17:00
Discussion





 PROTOCOLLO Home Page Other Workshop Informations
Speakers and Talks

Author: Michele Abrusci
Tiltle: ???
TimeSlot: 30 min.

ABSTRACT



Author: Gianluigi Bellin
Tiltle: A dual lambda-calculus of continuations in Polarized Bi-intuitionistic Logic
TimeSlot: 30 min.

ABSTRACT

We reconsider Rauszer's *bi-intuitionistic logic* in the framework of
the *logic for pragmatics*: every formula is regarded as expressing
an act of *assertion* or *conjecture*, where conjunction and implication
are assertive connectives and subtraction and disjunction are conjectural.
The resulting system of *polarized bi-intuitionistic logic* (PBL)
consists of two fragments, *positive intuitionistic logic*  LJ^{impl,and}
and *dual intuitionistic logic* LJ^{minus,or}, extended with two negations
("certainly not" and "it's doubtful that") partially internalizing the
duality between LJ^{impl,and} and LJ^{minus,or}.

Two modal interpretations and Kripke's semantics are considered, yielding
two logics: one, still called PBL, is interpreted over *bimodal preordered
frames* (W, R, S), where R and S are arbitrary preorders; the other,
called ILP_AC (intuitionistic logic for pragmatics of assertions and
conjectures) is intepreted over S4 (i.e., setting R = S); here negations
are indeed dualities.  

The conjectural fragment  LJ^{minus, or} is formalized by sequents of the
form
        C  => C_1, ..., C_n
or in Natural Deduction by derivations with *only one assumption* and
*multiple conclusions*. The term assignment has the form
        x: C  => t_1: C_1, ..., t_n: C_n

It is a *calculus of continuations* exhibiting several features of calculi
for concurrency, such as *broadcasting*, *remote binding* and *remote substitution*.  

The duality between LJ^{impl,and} and LJ^{minus,or} is extended from
formulas to proofs and it is shown that every computation in our calculus
of continuations is isomorphic to a computation in the simply typed lambda-calculus.

It is worth noticing the difference with existing term-assignments for
multiple-conclusion systems (such as those by Herbelin-Curien--Parigot and
Bierman-Urban); indeed, they essentially use "control terms"
        T: (Gamma |- Delta)
assigned to *sequents* rather than to *formulas in the succedent* and thus
in their calculi there is no trace of "concurrent interactions" between terms.   

The term-assignment is related to a categorical interpretation, which is
not given here. While categorical models for Rauszer's bi-intuitionistic
logic collapse to partial ordering (essentially, by Joyal's argument for
"Boolean categories"), it is quite clear how to construct a reasonable
(non-degenerate) categorical semantics for Polarized Bi-intuitionistic Logic.


Authors: Ugo Dal Lago
Title: On Light Logics, Uniform Encoding and Polynomial Time
TimeSlot: 30 min.

ABSTRACT

We investigate on the extensional expressive power of
Light Affine Logic, analysing the class of uniformly representable
functions for various fragments of the logic. We give evidence on the
incompleteness (for polynomial time) of the propositional
fragment. Following previous work, we show that second order leads to
polytime unsoundness. We then introduce simple constraints on second order
quantification and least fixpoints, proving the obtained fragment to be
polytime sound and complete.


Authors: Claudia Faggian and Francois Maurel
Title: Playing with graphs
Speaker: Claudia Faggian
TimeSlot: 30 min.

ABSTRACT

The  work we present steams both form Ludics and from the recent work in Game
Semantics,
which has been directed  to model more concurrent forms of interaction.

We introduce abstract structures corresponding to proof/programs 
(what is called strategy in Games Semantics  and design in Ludics),
which are graphs rather than trees.
Syntactically, this corresponds to working with abstract proof-nets
rather then abstract sequent calculus derivations (as in Girard's Ludics);
interactions are partial orders rather than linear sequences.
This way we relax sequentiality,  allowing for parallelism and
multi-focalization.



Authors: Arnaud Fleury
Title: Linear Bi-intuitionistic Logic
TimeSlot: 30 min.

ABSTRACT
 We present an analysis of bi-intuitionistic logic in the
tradition of C.Rauszer, W.Lawvere, R.Gore' and T.Crolard with the methods
of linear logic. It is well-known that *non-polarized* bi-intuitionistic
logic admits only degenerate categorical models: we describe tha syntax
and semantics for a *linear* bi-intuitionistic logic, where the tensor is
monoidal and the par pre-monoidal. The basic ideas of a game-semantics for
such a logic are sketched.



Authors: Pietro Di Gianantonio
Title: A game model for the nu-calculus
TimeSlot: 30 min.

ABSTRACT

 The nu-calculus is a simply typed lambda calculus having a basic type of
names. The primitives on names make the observational equivalence
nu-calculus quite subtle; only recently fully abstract game models for
nu-calculus as been proposed. In this talk I will present an alternative
and simpler game model for the nu-calculus.


Authors: Stefano Guerrini and Andrea Masini
Title: Proofs-Tests and Programs-Continuations
Speaker: Stefano Guerrini
TimeSlot: 30 minuti

ABSTRACT

Starting from the notion of "test" proposed by Girard we develop a
notion of test for intuitionistic logic.  We give a complete deductive
system for tests and we show that it is good to deal with
"continuations". In particular it is possible to use the
proposed system to work in a uniform way with Call by Value and Call
by Name translations.


Authors: Michele Pagani
Title: The problem of separation in Linear Logic
TimeSlot: 30 minuti

ABSTRACT

By taking inspiration from lambda-calculus ' observational equivalences
and the works on the injectivity of Linear Logic's semantics, we define
a syntactic and semantic notion of separation for linear logic proof-nets.
Two proof-nets R and R' are syntactically separable, if there exists a
context
C[] such that C[R] and C[R'] reduce to two different values (usually truth
and false); two proof-nets are semantically separable with respect to a
model M of LL, if their interpretation in M is different.
We discuss the question of separation for various computational systems
(lambda-calculus, lambda-mu calculus, ludics) and for the corresponding
fragments of LL.
Finally we give a counter-example to the syntactic (and semantic, with
respect to the coherent model) separability of polarized linear logic.


Authors: Luca Paolini, Elaine Pimentel and Simona Ronchi Della Rocca
Title: Lazy Strong Normalization
Speaker:
TimeSlot: 30 minuti

ABSTRACT

Among all the reduction strategies for the untyped
lambda-calculus, the so called lazy-beta-evaluation is
of particular interest due to its large applicability to
functional programming languages (e.g. Haskell). This
strategy reduces only redexes not inside a lambda abstraction.

The lazy strongly beta-normalizing terms are the
lambda-terms that don't have infinite lazy beta-reduction sequences.

This paper presents a logical characterization of
lazy strongly beta-normalizing terms using intersection types.
This characterization, besides being interesting by itself, allows
an interesting connection between call-by-name and call-by-value
lambda-calculus.

In fact, it turns out that the class of lazy strongly
beta-normalizing terms coincides with that of call-by-value potentially
valuable terms. This last class is of particular interest since it
is a key notion for characterizing solvability in the call-by-value setting.


Author: Elaine Pimentel, Simona Ronchi Della Rocca, Luca Roversi
Tiltle: Towards a proof-theoretical justification for Intersection Types
TimeSlot: 30 min.

ABSTRACT
It is well known that derivations in Intersection Types (IT) form
a strict subset of deductions in Intuitionistic Logic (LJ) -- up
to term decorations -- in the sense that IT imposes a
meta-theoretical restriction on proofs: conjunction can be
introduced only between derivations that are synchronized with
respect to the implication.

The goal of this work is to present a proof-theoretical
justification for IT. In particular, we discuss the relationship
between the intersection connective and the intuitionistic
conjunction. For this purpose, we define a new logical system
called Intersection Synchronous Logic (ISL), that proves
properties of sets of deductions of the implication-conjunction
fragment of LJ.

The main idea behind ISL is the decomposition of the
intuitionistic conjunction into two connectives, one with
synchronous and the other with asynchronous behavior.

Also in the present work, we prove that ISL enjoys both the
strong normalization and sub-formula properties as well as that
the Intersection Type assignment can be viewed as standard term
decoration of ISL.




Authors: Marco Pedicini e Francesco Quaglia
Title: PELCR: Parallel Environment for Lambda-Calculus Optimal Reduction
Speaker: Marco Pedicini
TimeSlot: 30 minuti

ABSTRACT

First we give short presentation of the theoretical background of PELCR
which is based on a particular way to compute the GOI execution formula.
Then, we show the kind of technical solutions we adopted
in the implementation in order to actual make parallel execution 
effective. We conclude with several theoretical questions
and open problems concerning further developments of the PELCR engine. A
computer demonstration of the software package  will be given in the
final part of the talk.


Author: Luca Roversi
Tiltle: Light languages and Primitive Recursive functions
TimeSlot: 30 minuti

ABSTRACT

The work, under development, deals with the problem of encreasing the
number of algorithms that can be programmed in paradigmatic programming
languages with predetermined complexity, derived from Linear Logic.
An experiment about how compositionally representing  recursively
defined functions is presented.
The experiment will suggest to introduce a language that:
*) is  polytime normalizing under a lazy reduction strategy
*) allows, to use !-boxes that can depend on more than one assumption.