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 run-time 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 normal-form is reached?" Termination assert that this problem is well-defined. 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 sub-field 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: Jean-Yves Marion Abstract: We investigate intrinsic characterizations of well-known 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 non-interference 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 Chung-Kil Hur ) Abstract: We construct operationally-based 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 step-indexing, give extensional and compositional specifications of when low-level code and values realize typed source-level terms. We prove full functional correctness of a compiler in terms of these relations and show how they also justify both source-level transformations and the linking of compiled code with hand-optimized code fragments that exploit non-parametric and non-functional low-level operations whilst being extensionally well-behaved. 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 call-by-name and call-by-value is extended to finite probabilistic computations. Moreover, a general equivalence result on the equilvalence of big-step and small-step semantics is given, with the help of co-inductive techniques. Title: Minimal unique expansion with digits in ternary alphabets Author: Anna Chiara Lai Abstract: The study of the redundancy of non-integer 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 non-integer base are unique, while for greater bases there exist some non-trivial unique expansions. By investigating an unespected relation between sturmian sequences and unique expansions, we explicitely characterize for a large class of three-letter 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 Faggian-Maurel-Curien’s ludics nets), we defined a new class of multiplicative/additive polarized proof nets, called J-proof nets. The distinctive feature of J-proof 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 J-proof 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 lambda-calculus, with constructors for algebraic data-types, pattern matching and recursive definitions, and thus allows for a natural programming style. The validity of LPL programs is checked through typing and a syntactic criterion on recursive definitions. The higher order type system is designed from the ideas of Light linear logic: stratification, 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 lambda-term, (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 constraint-based efficient (polynomial time) procedure. Title: Non idempotent intersection types into multiplicative linear logic Author: Jean-Marie Madiot Abstract: Intersection types characterize properties of lambda-terms 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 higher-order processes Author: Ugo Dal Lago (joint work with Simone Martini and Davide Sangiorgi) Abstract: We study the linearization of HOpi, a calculus for higher-order 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 (higher-order) 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 non-deterministic variants, including Ehrhard and Regnier's differential interaction nets. Title: The structural lambda calculus Author: Beniamino Accattoli Abstract: We present lambda-j, an untyped structural lambda-calculus with closures corresponding to lambda-j-dags, the graphical systems introduced by Accattoli and Guerrini which implements boxes by means of jumps. Lambda-j is a well behaved calculus (it enjoys confluence and preservation of beta-strong 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 lambda-j 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 XL-developments. Then, we show that lambda-j allows to reformulate Regnier's sigma-equivalence as a strong bisimulation. Last, we show that extending lambda-j with rules for composing or decomposing closures the obtained calculi still preserve lambda-calculus strong normalization. Title: Call-by-value 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 lambda-calculus 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 lambda-calculus, and where stratification is found to be equivalent to using actual first-order 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 non-deterministic variants, including Ehrhard and Regnier's differential interaction nets. Title: An additive type system for the linar-algebraic lambda-calculus Author: Alejandro Diaz-Caro and Barbara Petit Abstract: The linear-algebraic lambda-calculus [AD08] and the algebraic lambda-calculus [Vau07] extend the lambda-calculus 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 lambda-calculus with sums becomes the most basic object of study. We propose to study the role of sums within the linear-algebraic lambda-calculus 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 ready-to-use 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 plug-in 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 error-prone 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 high-level 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.
|
||||||||||||||||||||||||||||||||||||||||||||||||