Meeting on Logic and Complexity    (ProToCoLLo)

Bertinoro, 15th and 16th 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 proof-theroy.

It will take place just after the end of ICTCS03, on 15th afternoon.

The programme divides essentially in three parts:

Scheduling, short abstract on stable and informal talk subjects and a list of the participants follow.





Wednesday 15th afyternoon

15:30 -- 16:10

Talk A

16:10 -- 16:50

Talk C

16:50 -- 17:15


17:15 -- 17:55

Talk B

17:55 -- 18:40

Talk D

Thursday 16th morning

08:30 -- 09:20

Talk G

09:20 -- 10:10

Talk E

10:10 -- 10:30


10:30 -- 11:20

Talk G

11:20 -- 12:10

Talk F

12:10 -- 14:30


Thursday 16th afternoon

14:30 -- 16:00

“free discussions”

16:00 -- 16:30


16:30 -- 17:50

“free discussions”

17:50 -- 18:30

Talk H

Structured material and ideas

Martin Hoffman

A. Type systems for non-size-increasing functions.

Harry Mairson

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.

Katsushige Terui

B. Light Affine Logic simplified.

Ugo Dal Lago

C. Higher-Order Linear Ramified Recurrence (HOLRR) is a ptime sound and complete typed lambda caluclus. Its terms are those of a linear (affine) lambda-calculus -- 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.

Damiano Mazza

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.

Works in progress and informal ideas

Ugo Dal Lago

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 lambda-calculus. 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.

Damiano Mazza

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)