TLT – Types and Logic in Torino

22 September 2017

Colloquium in honor of Mariangiola Dezani-Ciancaglini, Simona Ronchi Della Rocca and Mario Coppo

This colloquium is a gathering for colleagues and friends who want to celebrate Mariangiola Dezani-Ciancaglini, Simona Ronchi Della Rocca and Mario Coppo, whose 70th birthdays take place between 2016 and 2017. Mariangiola, Simona and Mario are outstanding researchers in the community of theoretical computer science for their seminal contributions to the fields of λ-calculus, type theory and foundations of programming languages. They have been students of Corrado Böhm in the early 70's and spent most of their career at the Computer Science Department of the University of Torino, leading one of the largest research groups on formal methods for four decades. During this period they have been enthusiastic mentors for many young researchers now employed in prestigious institutions all over the world.

Pictures

Program

The seminars will take place in room Sala Multifunzione 1 of the Cavallerizza Reale located in Via Verdi 9, Torino.

14:30 – 14:45
Opening and greeting from Luca Console, head of the Computer Science Department.
Session 1
Chair: Ugo Montanari
14:45 – 15:30
Computational and Fine-Structure Aspects of Intersection Types
Jakob Rehof, Technische Universität Dortmund, Germany
Due to the enormous expressive power of the intersection type system the classical type theoretic decision problems (typability and inhabitation) are undecidable for the system. Still, many interesting and useful problems can be solved computationally, if we consider suitable restrictions, and from a logical standpoint it is interesting to investigate the fine-structure of the system. Results, challenges, and open problems for fragments and fine-structure of the system will be surveyed with a focus on computational aspects (algorithms and complexity) of associated decision problems, and some present and future application perspectives will be discussed.
Slides [PDF]
15:30 – 16:15
Stability in a Probabilistic Setting
Thomas Ehrhard, Université Paris Diderot - Paris 7, France
Probabilistic coherence spaces provide a model of Linear Logic which accommodates probabilistic functional programming. However it seems difficult to deal in this setting with probabilities on "continuous" measurable spaces such as the set of real numbers with the usual Lebesgue measurable sets. I will present a generalization of this model where types are interpreted as complete positive cones, which are normed semi-modules with non-negative real coefficients. The cone of all bounded measures on the real line is a typical object of this category. The main novelty is that, for proving cartesian closeness, we are led to require the morphisms to satisfy a kind of "hereditary monotonicity" condition which turns out to be equivalent to stability, when reformulated in coherence spaces. Joint work with Michele Pagani and Christine Tasson.
Slides [PDF]
16:15 – 16:45
Coffee break at the University of Torino historical building located in Via Verdi 8, Torino.
Session 2
Chair: Rocco De Nicola
16:45 – 17:30
Rule Formats for Nominal Operational Semantics
Luca Aceto, Gran Sasso Science Institute, L'Aquila, Italy, and Reykjavík University, Iceland
I will present some recent work on a nominal approach to operational semantics. The ultimate goal of this line of work is to give a general framework for the study of the semantics of languages involving binding operations, a research area to which Coppo, Dezani and Ronchi have given many seminal contributions.
Slides [PDF]
17:30 – 18:15
Mario and Mariangiola's Contributions to the Session Type Theory and Practice
Nobuko Yoshida, Imperial College London, UK
Since the year 2000, Mario and Mariangiola's research has been devoted to the study of session types for ensuring safety and liveness of communication protocols. Mariangiola first proposed a formalisation of Java with session types and later it was extended to asynchronous communications with Mario, which was later applied to the design and implementation of Session Java (SJ). These contributions initiated a flurry of research activity aiming at applying session types to many real-world programming languages. Mariangiola first studied a theory of progress in the session types for the pi-calculus, whose core theory was later extended with Mario to multiparty session types. This formalism became the core of the current version of an open-source protocol description language, Scribble, which is developed at Red Hat and Imperial. The Scribble language is used in the multi-million-USD Ocean Observatory Initiative project. I will talk about how their elegant works give the practical impacts to communication-intensive programming frameworks.
Slides [PDF]
18:15 - 18:30
Memorabilia
Mariangiola Dezani-Ciancaglini, Simona Ronchi Della Rocca and Mario Coppo, Università di Torino, Italy
Slides [PDF]
20:00 – 22:00
Dinner at Hafa Storie. A dinner speech will be delivered by Vladimiro Sassone.

Participation

The colloquium is open to everyone. Participants are required to register using this form and specifying TLT 2017 in the "Type of registration" field. The registration fee includes the cost of the dinner.

Early registration (on or before 24 July 2017) Late registration (on or before 19 Sep. 2017)
€70 €100

Venue

The colloquium will take place immediately after iFM 2017. Detailed information on the venue, including travel information and suggestions for accommodation, may be found in the corresponding sections of the iFM 2017 web site.

Organization