Meeting on
Logic and
Complexity
(ProToCoLLo)
Bertinoro, 15^{th} and 16^{th} October 2003
The idea is to bring together researchers involved in the italian national project “Protocollo”, one of whose research mainstreams is about implicit characterizations of computational classes, based, as much as possible, on structural prooftheroy.
It will take place just after the end of ICTCS03, on 15^{th} afternoon.
The programme divides
essentially in three parts:
Wednesday 15^{th} , in the afternoon: the most stable material and ideas, will be presented. The speakers will have slots of 40 minutes;
Thursday 16^{th} , in the morning: less formalized subjects and problems will be presented. The speakers will have slots of about 50 minutes whose sharing of time, between presentation and discussion, is up to the speakers;
Thursday 16^{th} , in the afternoon: free discussion, may be in separate groups, each working on one the subjects, illustrated in the morning, or something related. We shall conclude by a talk by Harry Mairson on a topic not directly related with the meeting topics, but which involves linear logic technology, so it is related to the whole Protocollo project.
Scheduling, short abstract on stable
and informal talk subjects and a list of the participants follow.
Day 
Hour 
Activity 

Wednesday 15^{th} afyternoon 
15:30  16:10 


16:10  16:50 


16:50  17:15 
Coffebreak 

17:15  17:55 


17:55  18:40 

Thursday 16^{th} morning 
08:30  09:20 
Talk G 

09:20  10:10 


10:10  10:30 
Coffebreak 

10:30  11:20 


11:20  12:10 


12:10  14:30 
Lunch 
Thursday 16^{th} afternoon 
14:30  16:00 
“free discussions” 

16:00  16:30 
Coffebreak 

16:30  17:50 
“free discussions” 

17:50  18:30 
A. Type systems for nonsizeincreasing functions.
I. The talk is about some observations on Wadler's ICFP paper "Call by value is dual to call by name": I think better results can be stated.
B. Light Affine Logic simplified.
C. HigherOrder Linear Ramified Recurrence (HOLRR) is a ptime sound and complete typed lambda caluclus. Its terms are those of a linear (affine) lambdacalculus  every variable occurs at most once  extended with a limited recursive scheme on a word algebra. Completeness for ptime holds by embedding Leivant's ramified recurrence on words into HOLRR. Soundness is established at all types  and not only for first order terms. Type connectives are limited to tensor and linear implicaation. Moreover, typing rules are given as a simple deductive system.
D. Danos e Joinet define Elementary Linear Logic {ELL} as a subsystem of Linear Logic {LL} whose derivations satisfy a couple of structural constraints. The approach is extended to characterize deterministic polynomial computations.
E. The paper where Lafont introduces Soft Linear Logic, concludes with some suggestions about how to obtain an elementary version of SLL. The idea is to discuss about such seggestions.
F. Elementary and Light logics can be used as type assignments for the untyped lambdacalculus. Given an untyped lambda term M and a type derivation \pi for M, it is possible to compute (in time O(pi)) a bound to the number of reduction steps to the normal form of M. The discussion is about the possibility of improving the quality of such a bound.
G. The goal of this discussion is to understand why “light logics” work. The starting point is to show examples of computations inside Linear and Classical logics which are not elementary.
H. The definition of SLL, by Lafont, is not completely under control: the goal is to clarify some points about syntax, polytime soundness and completeness.
Paolo Coppola (Udine)
Martin Hoffman (Munich)
Ugo Dal Lago (Bologna)
Harry Mairson (Boston  MA)
Simone Martini (Bologna)
Damiano Mazza (Marseille)
Simona Ronchi Della Rocca (Torino)
Luca Roversi (Torino)
Katsushige Terui (Tokio)
Lorenzo Tortora De Falco (Roma)