LOCATION: Scuola di ApplicazioneAula 201Via Arsenale 22  Torino (5 minuti a piedi dall'hotel Bologna) Titles and Abstracts Informal Workshop on Implicit Computational ComplexitySpeaker: Ugo Dal LagoTITLE: 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 supinterpretation ABSTRACT:We propose a new method to control memory resources by static analysis. For this, we introduce the notion of supinterpretation 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 quasiinterpretations 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, lambdacalculus and Intersection Types (joint work with Simona Ronchi Della Rocca) ABSTRACT: A type assignment system is presented, assigning to terms of lambdacalculus formulas of Lafont’s Soft Linear Logic. The aim is to allow the use of lambdacalculus 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 MeetingSpeaker: Fabio AlessiTITLE: 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 machineindependent 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 proofnet. 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 proofnets 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 0obsessional (resp. tobsessional 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, objectoriented programming, contesti (ovviamente), e metaprogramming. 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
