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

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

• Speaker: Corrado Boehm
  Title: The scientific works of Coppo, Dezani and Ronchi
  Abstract. Some of the results obtained by CDR are analysed from an historical and methodological viewpoint, then compared with the current developments of computer science (software and hardware). We also consider relations with the trends and applications in fields like logic, mathematics, physics, and engineering. We are particularly interested in the connections with biology and the theory of knowledge.
  

• Speaker: Chantal Berline (CNRS - Université Paris 7; Equipe PPS)
  Title: Can a proper lambda-model have an r.e. equational theory ?
  Abstract. By a proper lambda-model we understand here a model M of untyped lambda-calculus whose construction makes no reference to the syntax of lambda-calculus.
  I will present here several results obtained jointly with Antonino Salibra and Giulio Manzonetto, and which all argue in favour of the following conjecture, where "r.e". stands for "recursively enumerable":
  Conjecture: No proper lambda-model can have an r.e. equational theory.
  Variant: No lambda-model living in Scott's semantics or in one of its refinement (e.g. the stable or strongly stable semantics) can have an r.e. equational theory.
  Note that this conjecture encompasses the longstanding open question of the existence of a proper model having lambda-beta as its equational theory.
  We will see in particular that we can prove that no "effective" lambda-models can have an r.e theory, at least if it lives in the stable or in the stable semantics; concerning Scott's continuous semantics, we have only partial results, even for effective graph models. Nevertheless, these partial results cover all the lambda-models which have been introduced "individually" in the literature.
  Bibliography (see: http://www.pps.jussieu.fr/~berline/ ):
  • Chantal Berline, Giulio Manzonetto and Antonino Salibra. Lambda theories of effective lambda models.

• Speaker: Furio Honsell
  Title:
  Abstract.
  

• Speaker: Giuseppe Longo (CNRS et Dépt. d'Informatique. École Normale Supérieure, Paris)
  Title: Symmetries in Foundations
  Abstract. Our mathematical relation to space originated by the symmetries at the core of Greek geometry as well as Riemann's manifolds. Symmetries continued to provide the conceptual tools for further constructions of mathematical structures, from Poincare''s Geometry of Dynamical Systems to Category Theory, but were disregarded in logical foundations as Arithmetic has been considered, since Frege, the (only or paradigmatic) locus for foundational analyses. They are back now also in Logic, but a direct link to their role in Physics is still missing. As a matter of fact, geodetic principles, in Physics, originate in symmetries and provide an effective foundational frame for the main theoretical approaches, since the work by E. Noether and H. Weyl. The common "construction principles", largely grounded on symmetries, may renew the foundational links between these two disciplines. Can computability fit into this renewed frame? What can it tell us about physical dynamics?
  Main reference (see: http://www.di.ens.fr/users/longo ):
  • Bailly F., Longo G. Mathématiques et sciences de la nature. La singularité physique du vivant. Hermann, Paris, 2006 (Introduction in English downloadable)

• Speaker: Henk Barendregt
  Title: Proving the range property for lambda theories and models
  Abstract. The range property states that the range of a definable map has cardinality either one or infinite. In several situations this has been proved by different means: topology, computability, analysis of reduction. Is there a common pattern?
  

• Speaker: Pawel Urzyczyn
  Title: Proof search in propositional intuitionistic logic
  (Joint work with Morten H. Sorensen)
  Abstract. In 1938 Mordchaj Wajsberg proved that intuitionistic propositional connectives are not definable from each other. For this, he developed a proof search algorithm, a forerunner of the Ben-Yelles inhabitation algorithm. We discuss the (now quite forgotten) Wajsberg algorithm and the characterization of normal forms it induces. We extend this characterization to second-order propositional logic (with all the standard connectives and existential quantification) and apply it to give a purely syntactic Loeb-style translation from first-order to second-order propositional intuitionistic logic.