CONCERTOControllo e certificazione dell'uso delle risorse 

::
Home
:: Preliminary Schedule :: Participants :: Accomodation :: Kickoff meeting 
The final meeting of CONCERTO will take place in Torino
at the 'Scuola di Applicazione  Palazzo dell'Arsenale',
from June 09 to June 11, 2010. Palazzo
dell'Arsenale is in the city center of Torino in via dell'Arsenale
22 (map) The following is a tentative scheduling.
Thursday, June 10th
20:00 Social dinner at 'Porto di Savona'  piazza Vittorio Veneto 2, Torino (map) Friday, February 11th
Invited Talks Title: Probabilistic Types and Polymorphism Author: Alessandra Di Pierro Abstract: We present a novel theory of types where formulas may contain a choice constructor; this constructor allows for the selection at runtime of a particular type among a finite set of options, all associated with a given probability. We show that this theory is able to express a new form of polymorphism, called probabilistic polymorphism, which allows us to probabilistically select the code of a polymorphic function to be executed. It also induces a type assignment system for a probabilistic lambda calculus which we show to be sound with respect to a probabilistic term reduction. Title: Automated Complexity of Analysis of Rewriting Author: Georg Moser Abstract: For a terminating term rewrite system (TRS for short), we can consider the following abstract problem: "How many rewrite steps can we perform till no a normalform is reached?" Termination assert that this problem is welldefined. This question entails investigations into the "complexity" of term rewrite systems. A TRS is considered of higher complexity, if the number of possible rewrite steps is larger. In recent years this subfield of rewriting has been thoroughly revived and a shift towards automation has been performed. In the talk I will review recent results and discuss the strong links to implicit computational complexity theory as well as to the field of automated complexity analysis of programs. Title: A type system for complexity flow analysis Author: JeanYves Marion Abstract: We investigate intrinsic characterizations of wellknown complexity classes. We develop a type system for an imperative programming language to bound program runtimes. The type system is based on secure information flow typing, which has been widely studied. Intuitively, program variables are classified as either low or high. We wish to prevent information from flowing from low variables to high variables. We prove noninterference results, which basically say that values of high variables are independent from values of low variables. Thus, we establish a closed relation with ramified recursion, which is used in implicit computational complexity. We also deal with declassification in order to delineate a broad class of programs. Finally, we provide a characterization of the class of polynomial time functions. Title: Realizability and Compositional Compiler Correctness for a Polymorphic Language Author: Nick Benton ( joint work with ChungKil Hur ) Abstract: We construct operationallybased realizability relations between phrases in a language with both universal and existential types and programs for a variant SECD machine. The relations, defined using parametricity, biorthogonality and stepindexing, give extensional and compositional specifications of when lowlevel code and values realize typed sourcelevel terms. We prove full functional correctness of a compiler in terms of these relations and show how they also justify both sourcelevel transformations and the linking of compiled code with handoptimized code fragments that exploit nonparametric and nonfunctional lowlevel operations whilst being extensionally wellbehaved. The definitions and results have been fully formalized in the Coq proof assistant. Contributed Talks Title: A probabilistic lambda calculus  some preliminary investigations Author: Margherita Zorzi (joint work with Ugo Dal Lago) Abstract: We propose a probabilistic extension of the pure, untyped lambda calculus. The syntax is enriched with a choice operator and, as a consequence, terms can evaluate to (finite or infinite) sets of observable results. We are exploring several research directions whose aim is giving foundations to probabilistic functional programming. The classical CPS simulation between callbyname and callbyvalue is extended to finite probabilistic computations. Moreover, a general equivalence result on the equilvalence of bigstep and smallstep semantics is given, with the help of coinductive techniques. Title: Minimal unique expansion with digits in ternary alphabets Author: Anna Chiara Lai Abstract: The study of the redundancy of noninteger base numeration systems involves several fields of mathematics and of theoretical computer science, including number theory, ergodic theory, topology, combinatorics on words. When the base is smaller than a sharp value, called critical base, only trivial expansions in noninteger base are unique, while for greater bases there exist some nontrivial unique expansions. By investigating an unespected relation between sturmian sequences and unique expansions, we explicitely characterize for a large class of threeletter alphabets the minimal unique expansions, namely those unique expansions that rst appear when we choose bases larger than the critical base. Title: Jump from parallel to sequential proofs: exponentials Author: Paolo Di Giamberardino Abstract: In previous works, by importing ideas from game semantics (notably FaggianMaurelCurien’s ludics nets), we defined a new class of multiplicative/additive polarized proof nets, called Jproof nets. The distinctive feature of Jproof nets with respect to other proof net syntaxes, is the possibility of representing proof nets which are partially sequentialized, by using jumps (that is, untyped extra edges) as sequentiality constraints. Starting from this result, in the present work we extend Jproof nets to take into account erasing (weakening) and duplication (contraction). More precisely, we show how using jumps makes possible to define nets where the usual nesting condition on boxes is relaxed, allowing a partial superposition of boxes. Moreover, we prove that, even in case of ’’superposed’’ boxes, reduction still enjoys confluence and strong normalization, using Gandy’s method to prove strong normalization, following the work of Pagani and Tortora de Falco. Title: A PolyTime Functional Language from Light Linear Logic Author: Virgile Mogbil Abstract: We introduce a typed functional programming language LPL in which all valid programs run in polynomial time, and which is complete for polynomial time functions. LPL is based on lambdacalculus, with constructors for algebraic datatypes, pattern matching and recursive deﬁnitions, and thus allows for a natural programming style. The validity of LPL programs is checked through typing and a syntactic criterion on recursive deﬁnitions. The higher order type system is designed from the ideas of Light linear logic: stratiﬁcation, to control recursive calls, and weak exponential connectives §, !, to control duplication of arguments. Title: Type Inference in Intuitionistic Linear Logic Author: Patrick Baillot (joint work with Martin Hofmann) Abstract: We study the type checking and type inference problems for intuitionistic linear logic: given a System F typed lambdaterm, (i) for an alleged linear logic type, determine whether there exists a corresponding typing derivation in linear logic (type checking) (ii) provide a concise description of all possible corresponding linear logic typings (type inference). We solve these problems using a novel algorithmic type system for linear logic, which leads to a constraintbased efficient (polynomial time) procedure. Title: Non idempotent intersection types into multiplicative linear logic Author: JeanMarie Madiot Abstract: Intersection types characterize properties of lambdaterms such as head, weak, strong normalization. One can establish relations between intuitionistic logic and intersection types with idempotency. Here we consider a typing system without idempotency and we underline common traits with intuitionistic multiplicative linear logic. We analyse head normalization to try and get consistency properties such as completeness and soundness or, more precisely, subject reduction/expansion. Title: Linearizing higherorder processes Author: Ugo Dal Lago (joint work with Simone Martini and Davide Sangiorgi) Abstract: We study the linearization of HOpi, a calculus for higherorder processes. Ordinary transmission of processes through channels is decomposed into forwarding (which is linear) and copying, in the spirit of linear logic. This opens up the possibility of importing techniques like stratification and boundedness into the realm of (higherorder) process calculi. Title: The algebra and geometry of commitment Author: Felice Cardone Abstract: I propose a formal description, by means of graphical and categorical structures, of mechanisms for handling the dynamics of rights and obligations familiar in jurisprudence. It will be argued that the formal study of commitment in this setting can contribute new insights to the analysis of a large variety of communicative situations, in particular the dialogical interpretation of logic. Title: Geometry of Interaction: stream specification and implementation Author: Marco Pedicini Title: Measuring the Expressiveness of Rewriting Systems through Event Structures  part I Author: Damiano Mazza Abstract: We develop a methodology for studying and comparing the expressiveness of computational models which are based on rewriting. We consider a class of rewriting systems, which we call normal, admitting a natural interpretation in terms of event structures; this is done by building up on work of Mazurkiewicz, Nielsen, Plotkin, Winskel, Melliès, and Mimram. Then, we introduce the notion of bisimilar embedding of event structures, which allows us to say when a computational system is "at least as expressive" as another one, as soon as these two are described in terms of event structures. Finally, we prove a few separation results for normal rewriting systems based on this notion, and we give an application of these to interaction nets and their nondeterministic variants, including Ehrhard and Regnier's differential interaction nets. Title: The structural lambda calculus Author: Beniamino Accattoli Abstract: We present lambdaj, an untyped structural lambdacalculus with closures corresponding to lambdajdags, the graphical systems introduced by Accattoli and Guerrini which implements boxes by means of jumps. Lambdaj is a well behaved calculus (it enjoys confluence and preservation of betastrong normalisation) with only four rewriting rules corresponding to the multiplicative and exponential rules of linear logic. The novelty with respect to other calculi is that the rules act at a distance and on the base of multiplicities. We use lambdaj to revisit some rewriting properties of lambda calculus and substitutions. We give new characterizations of lambda calculus full developments and superdevelopments, based on a linear analysis of redex creations, and we introduce the new and more general notion of XLdevelopments. Then, we show that lambdaj allows to reformulate Regnier's sigmaequivalence as a strong bisimulation. Last, we show that extending lambdaj with rules for composing or decomposing closures the obtained calculi still preserve lambdacalculus strong normalization. Title: Callbyvalue simulation in combinatory logic Author: Paolo Parisen Toldin Abstract: In this talk I focus on the problem of simulating reduction strategies in Combinatory Logic. It is well known that through a standard translation from Lambda Calculus to CL it is easy to simulate LC reduction steps in CL. In the literature some works have proposed simulations of reduction strategies by means of CL. Unfortunately all such proposal need to extend the CL framework. Here we investigates how to directly define strategies in CL with no extension. Title: Types and effects seen through Linear Logic Author: Paolo Tranquilli Abstract: Types and effects systems allow to statically analyze impure side effects in programs, of which a prime example is memory access. The typical approach is to abstract memory locations into a finite set of regions. Recently Boudol and later Amadio have proposed a region stratification discipline ensuring termination of variants of lambdacalculus with memory access operations. The stratification discipline may seem somewhat unfamiliar. As it turns out however, there is a monadic translation (in Moggi's sense) that simulates memory operations in ordinary lambdacalculus, and where stratification is found to be equivalent to using actual firstorder types rather than recursive ones. I will present this core observation through the looking glass of linear logic proofnets, which have the advantage of unearthing the parallel evaluation potential of types and effects system and opening the way to a treatment of multithreading via differential nets. Title: Measuring the Expressiveness of Rewriting Systems through Event Structures  part II Author: Damiano Mazza Abstract: We develop a methodology for studying and comparing the expressiveness of computational models which are based on rewriting. We consider a class of rewriting systems, which we call normal, admitting a natural interpretation in terms of event structures; this is done by building up on work of Mazurkiewicz, Nielsen, Plotkin, Winskel, Melliès, and Mimram. Then, we introduce the notion of bisimilar embedding of event structures, which allows us to say when a computational system is "at least as expressive" as another one, as soon as these two are described in terms of event structures. Finally, we prove a few separation results for normal rewriting systems based on this notion, and we give an application of these to interaction nets and their nondeterministic variants, including Ehrhard and Regnier's differential interaction nets. Title: An additive type system for the linaralgebraic lambdacalculus Author: Alejandro DiazCaro and Barbara Petit Abstract: The linearalgebraic lambdacalculus [AD08] and the algebraic lambdacalculus [Vau07] extend the lambdacalculus allowing linear combinations of terms. A variant of these calculi provides sums of terms without coefficients (which nearly amounts to having natural numbers as coefficients). In fact, most calculi associated with differential linear logic are presented without coefficients. Thereby, the lambdacalculus with sums becomes the most basic object of study. We propose to study the role of sums within the linearalgebraic lambdacalculus from a logical point of view. First we introduce an extension of System F with sum operator for types. Then we interpret it into a fragment of Linear Logic. Title: Linearity: syntax vs. semantics Author: Luca Paolini (joint work with Marco Gaboardi and Mauro Piccolo) Title: Automatic Generation of Cryptographic Code  Chapter Binary Elliptic Curves Author: Emanuele Cesena (joint work with Daniele Canavese) Abstract: Implementation of cryptographic primitives is a crucial task in applied cryptography. The history of cryptography shows that a primitive coming with a rich mathematical structure usually leads to an elegant description, simple to be understood, used and developed by a human. This richness from the theoretical point of view, however, introduces difficulties in the tasks of formally model, treat and more in general implement the same primitive on a computer. Furthermore, optimization techniques that are required to increase performance (and sometimes just to achieve a minimum level of functionality) are often vectors for errors and vulnerabilities. In this work we present a framework for automatic generation of cryptographic code, for testing and for packaging readytouse libraries, focusing on elliptic curve cryptography, in particular on binary elliptic curves. The code generator, which is the core of the framework, is designed to create greatly optimized code and to be extensible, allowing programmers to add new algorithms through a plugin mechanism. The generator is an actual compiler that translates from an higher level language into C or C++, taking care of specific optimization which are tedious and errorprone from a programmer perspective. The corresponding high level code is much more simple (and small), and this guarantees higher maintainability. In future works we plan to extend the generator in several directions: to support alternative highlevel languages (e.g., functional languages), to provide code annotation (useful, e.g., to formally prove properties of the generated code), to improve the capability of optimization and, of course, to support a wider set of cryptographic algorithms. Author: Marco Gaboardi (joint work with Ugo Dal Lago) Abstract: We present a work in progress aiming at providing a general framework for implicit computational complexity. By means of dependent types and dependent modality in a linear setting we can formally reflect at the type level the program evaluation complexity. This fact allow us to obtain implicit characterizations of complexity classes that are complete in terms of programs reducing the class membership problem to a corresponding constraint satisfaction problem.
