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