LOCATION: Scuola di Applicazione

Aula 201
Via Arsenale 22 - Torino
(5 minuti a piedi dall'hotel Bologna)

Titles and Abstracts

Informal Workshop on Implicit Computational Complexity

Speaker: Ugo Dal Lago
TITLE: On the intensional expressive power of bounded calculi.
ABSTRACT: I will sketch an obvious result on Cobham's Bounded Recursion on Notation. Then, I will revisit Girard, Scedrov and Scott's Bounded Linear Logic, with particular emphasis on its intensional expressive power.

Speaker: Romain Pechoux
TITLE:Resource analysis by sup-interpretation
ABSTRACT:We propose a new method to control memory resources by static analysis. For this, we introduce the notion of sup-interpretation which bounds from above the size of function outputs. This method applies to first order functional programming with pattern matching. This work is related to quasi-interpretations but we are now able to determine resources of more algorithms and it is easier to perform an analysis with this new tools.

Speaker:Marco Gaboardi
TITLE: Soft Linear Logic, lambda-calculus and Intersection Types (joint work with Simona Ronchi Della Rocca)
ABSTRACT: A type assignment system is presented, assigning to terms of lambda-calculus formulas of Lafont’s Soft Linear Logic. The aim is to allow the use of lambda-calculus as programming language, where types are used to assure the termination of a program in polinomial time. Moreover by allowing a (restricted form) of intersection as type constructor, the set of algorithms that can be written in the typed language increases, while preserving the complexity limit.

Annual Project's Meeting

Speaker: Fabio Alessi
TITLE: Soluzioni estese di equazioni di dominio.
ABSTRACT: Si generalizza la classica tecnica di Scott (computo del limite diretto) per ottenere "special purpose" modelli del lambda calcolo.

Speaker: Ugo Dal Lago
TITLE: Context Semantics and Implicit Computational Complexity
ABSTRACT: Implicit Computational Complexity aims at giving machine-independent characterizations of complexity classes based on mathematical logic. Context semantics has been introduced by Gonthier, Abadi and Levy as a model of Geometry of Interaction and has been shown useful in proving correctness of optimal reduction algorithms. Interestingly, the intensional nature of context semantics can be exploited in proving correspondences between logical systems and complexity classes. We illustrate some of these results, namely some correspondences between subsystems of Godel's T and complexity classes. Moreover, we explain how context semantics can give precise information on the time needed to normalize any linear logic proof-net.

Speaker: Paolo Tranquilli
TITLE: Typing Problems in Second Order Light Logics
ABSTRACT: Typing problems have a meaningful role regarding an implementation of light logics as type assignment programming disciplines, while second order is necessary to gain expressiveness. However Type Checking and Typability have been proved undecidable for system F. Adapting the proof, it is shown that Type Checking is undecidable for a variety of systems (DLAL, LAL, EAL).

Speaker: Marco Pedicini
TITLE: Supporting Function Calls within PELCR
ABSTRACT: In [PediciniQuaglia2000], [PediciniQuaglia2005}, PELCR has been introduced as an implementation derived from the Geometry of Interaction in order to perform virtual reduction on parallel/distributed computing systems. In this work we provide an extension of PELCR with computational effects based on directed virtual reduction \cite{DPR97}, namely a restriction of virtual reduction \cite{DanosRegnier93}, which is a particular way to compute the Geometry of Interaction \cite{Girard89a} in analogy with Lamping's optimal reduction \cite{Lamping90}. Moreover, the proposed solution preserves scalability of the parallelism arising from local and asynchronous reduction as studied in \cite{PQ2005}.

Speaker: Roberto Maieli
TITLE: Criteri di correttezza per le reti di MALL
ABSTRACT: We present a theory of MALL proof-nets satisfying the following conditions:
- proof structures must be simple (like in the MLL case), without special conditions (like ``weights'', ecc...); - cut reduction must be "local" (with only local single steps of cut reduction), terminating and confluent; - correctness criterion must be stable under cut reduction, adequate and sequentializable.

Speaker: Lorenzo Tortora de Falco (joint work with O. Laurent)
TITLE: Obsessional cliques: a semantic characterization of bounded time complexity
ABSTRACT:We propose a new approach to the semantics of proofs of light systems, and we expound the first result of this approach: relative completeness. The idea is to choose a light system and a denotational model of Linear Logic (LL), and to prove that an LL proof is a proof of the chosen light system iff its interpretation satisfies some given (semantic) property. We choose as light logical systems ELL for elementary time and SLL for polynomial time, as model the relational one (but coherent semantics would also do) and we prove that an LL proof is a proof of ELL (resp. SLL) iff its interpretation is 0-obsessional (resp. t-obsessional from some t).

Speaker: Antonino Salibra
TITLE: Models of lambda calculus as sheaves over Boolean spaces
ABSTRACT: In this talk we show that, against common belief, combinatory algebras satisfy interesting algebraic properties. The results are applied to the models of lambda calculus.

Speaker: Ruggero Pagnan
TITLE: Type theory via category theory
ABSTRACT: We distinguish between three basic kinds of type theory: simple, dependent and polymorphic on the base of the different form of type theoretic indexing. Fibered category theory can be thinked of as ordinary category theory over a base category. As a logic is always a logic over a type theory so a category capturing the logic is fibered over a category capturing the underlying type theory.
Speaker: Murdoch Gabbay
TITLE: The NEW calculus of contexts
ABSTRACT: Un tratto caratteristico del lambda calcolo e` "funzioni come dati".  Io parlero` di un'estenzione del lambda calcolo dove ci sono anche "contesti come dati".  Dimostrero` che la maggiore potenza espressiva unifica numerosi aspetti dei linguaggi di programmazione, fra cui unstructured datatypes, object-oriented programming, contesti (ovviamente), e meta-programming.

Speaker: Paolo Di Giamberardino
TITLE: A jump from parallel to sequential proofs
ABSTRACT: In this talk we introduce proof nets with jumps, a variation of linear logic's proof nets which allow to deal with objects with different degree of sequentiality, and we prove a sequentialisation theorem for them.

Time Table

Wednesday  18th January 2006
(Informal Workshop on Implicit Computational Complexity)
14:30 -- 15:30
 Ugo Dal Lago : On the intensional expressive power of bounded calculi.
 (30 min. of discussion)
15:30 -- 16:30
 Marco Gaboardi : Soft Linear Logic, lambda-calculus and ...
 (30 min. of discussion)
16:30 -- 17:00
17:00 -- 18:00
 Romain Pechoux : Resource analysis by sup-interpretation.
 (30 min. of discussion)
18:00 -- 18:30
 Problems Session

Thursday 19th January 2006
(Annual Project's Meeting)
09:30 -- 10:00
10:00 -- 11:00
 Tutorial: Proof Theory as a Control Theory
 by Stefano Guerrini and Andrea Masini
11:00 -- 11:30
11:30 -- 12:00
 Roberto Maieli: Criteri di correttezza per le reti di MALL.
12:00 -- 12:30
 Marco Pedicini: Supporting Function Calls within PELCR
12:30 -- 14:30
14:30 -- 15:30
 Tutorial: Implicit Computational Complexity
 by Ugo Dal Lago and Simone Martini
15:30 -- 16:00
 Murdoch Gabbay: The NEW calculus of contexts
16:00 -- 16:30
16:30 -- 17:00
 Ugo Dal Lago: Context Semantics and Implicit Computational Comp ...
17:00 -- 17:30   Ruggero Pagnan: Type theory via category theory.
 Social dinner

Friday 20th January 2006
(Annual Project's Meeting)
09:30 -- 10:30
 Tutorial: Parametric Lambda Calculus
 by Simona Ronchi Della Rocca and Luca Paolini
10:30 -- 11:00
 Fabio Alessi : Soluzioni estese di equazioni di dominio.
11:00 -- 11:30
11:30 -- 12:00
 Lorenzo Tortora de Falco: Obsessional cliques .....
12:00 -- 12:30   Paolo Di Giamberardino: A jump from parallel to sequential proofs
12:30 -- 13:00   Antonino Salibra: Models of lambda calculus as sheaves over .....
13:00 -- 13:30   Paolo Tranquilli: Typing Problems in Second Order Light Logics
13:30 -- 15:30
15:30 -- 17:00   Final Discussions and Business meeting
17:00 -- 17:30   Coffe Break