|Program||This colloquium is organised to celebrate the 60th birthday of Mario Coppo , Mariariangiola Dezani-Ciancaglini , and Simona Ronchi Della Rocca|
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".