Types and Computations:
A Colloquium in Honor of
Mario Coppo,
Mariangiola Dezani-Ciancaglini,
Simona Ronchi Della Rocca

Wednesday, October 3, 2007, Roma
in conjunction with ICTCS 2007

Program This colloquium is organised to celebrate the 60th birthday of Mario Coppo , Mariariangiola Dezani-Ciancaglini , and Simona Ronchi Della Rocca
08.30-09.00 Registration and Opening

Session 1: Chair Rocco De Nicola
09.00-10.00 Invited Talk,
Corrado Boehm .
The scientific works of Coppo, Dezani and Ronchi
( talk, in Italian )
10.00-11.00 Invited Talk,
Chantal Berline .
Can a proper lambda-model have an r.e. equational theory?

11.00-11.30 Coffee Break

Session 2: Chair Eugenio Moggi
11.30-12.30 Invited Talk,
Furio Honsell .
Intersection types, (more than) 25 years on, the adventure continues: theories, coalgebras, games,...

12.30-14.00 Lunch

Session 3: Chair Simone Martini
14.00-15.00 Invited Talk,
Giuseppe Longo .
Symmetries in Foundations

15.00-15.30 Coffee Break

Session 4: Chair Vladimiro Sassone
15.30-16.30 Invited Talk,
Henk Barendregt .
Proving the range property for lambda theories and models
16:30-17:30 Invited Talk,
Pawel Urzyczyn .
Proof search in propositional intuitionistic logic

20.00 Social Dinner
The 60th birthdays of Mario Coppo, Mariangiola Dezani-Ciancaglini, and Simona Ronchi Della Rocca all take place between 2006 and 2007. These three researchers are widely known in the world community of theoretical computer scientists, and especially among the researchers in lambda-calculus, type theory and semantics of programming languages.

All of them have been students of Corrado Boehm in the early 70's, and got a professorship of Computer Science by the University of Torino, where they have been the first members of the "lambda-group", still the largest group in the field.

Since then they worked on interleaving fields over thirty years and more. For the common part of the large bibliography that will appear in a forthcoming volume dedicated to them, it seems worthy to mention the introduction of intersection types, a fruitful extension of Curry's assignment system allowing for a deep understanding of the relation between syntax and semantics of the lambda-calculus. Among the results we mention separability and approximation theorems, the studies on typability and principal type schemes for polymorphic systems, the completeness theorem for Curry assignment systems and the construction of filter lambda-models.

Beside the common kernel of interests and research work, each of them has pursued her/his own investigation into several aspects of the semantics of calculi and type systems. Coppo contributed on recursive types proposing a new denotational interpretation; he used assignment systems for the static analysis of programs, with applications to strictness, totality and dead-code analysis; he also investigated the connection between type assignment and abstract interpretation. Dezani investigated union types, both for the lambda-calculus and for its nondeterministic and parallel extensions. She exploited type systems to study the behaviour of concurrent and mobile processes, enforcing safe and structured interaction. She studied type systems for object oriented languages allowing for strong forms of polymorphism and modularity; these eventually meet the foundational work on typing process calculi when concurrent objects and session types are involved. Ronchi has studied typability in the case of polymorphic and dependent types, both with respect to the characterization of the set of typable terms, and to (semi)algorithms for type reconstruction. She introduced and studied a hierarchy of assignment systems that parallels Barendregt's lambda-cube. Concerning lambda-calculi denotational semantics she established the incompleteness of topological models, and extended the notion of filter models to qualitative domains and to coherent spaces, in view of understanding in particular the lazy and call-by-value lambda-calculi. This led both to works on linear logic, and to a systematic presentation of "parametric lambda-calculi".

Abstract of the talks

To contact the organizers: cdr60 at di dot unito dot it
Last update: Tuesday, 08-Jan-2008 10:16:59 CET