28-29 June 2007
From Type Theory to Morphologic Complexity:
A Colloquium in Honor of Giuseppe Longo
In conjunction with RDP 2007.
Paris, Conservatoire National des Arts et Métiers, Amphitheaters 3 and A.
This colloquium was organised to celebrate the 60th birthday of Giuseppe Longo. Some photos of the meeting can be found here.

The main research area Giuseppe Longo has been interested in concerns syntactic and semantic properties of the "logical base" of functional languages: Combinatory Logic, Lambda-calculus and their extensions. However, he always investigated these topics in its broadest setting which relates them to Recursion Theory, Proof Theory and Category Theory.

In this perspective, Longo worked at some aspects of Recursion Theory, Higher Type Recursion Theory, Domain Theory and Category Theory as part of a unified mathematical framework for the theory and the design of functional languages. In a sense, Longo has always been mostly interested in the "interconnecting results" or "bridges" and applications among different areas and to language design. He also worked at the applications of functional approaches to Object-Oriented programming. He is currently extending his interdisciplinary interests to Philosophy of Mathematics and Cognitive Sciences.

A recent interdisciplinary project on Geometry and Cognition (started with the corresponding grant: "Géométrie et Cognition", 1999 - 2002 with J. Petitot et B. Teissier), focused on the geometry of physical and biological spaces. The developements of this project lead to a new initiative at DI-ENS, in 2002, the setting up of the research team "Complexité et information morphologiques" (CIM), centered on foundational problems in the interface between Mathematics, Physics and Biology.

This colloquium tries to partially cover the various fields spanned by Giuseppe Longo research via several talks given by some of the collegues he met during his quest.

Speakers and talks (alphabetical order)
  • Henk Barendregt and Jan Willem Klop: Non-left linear reductions via infinitary lambda calculus
    [Abstract] In this paper we treat two cases where an infinitary treatment yields interesting finitary results. (1) Adding non-left-linear reduction rules such as Dxx → x or the reduction rules for Surjective Pairing to the lambda calculus yields non-confluence, as was proved in Klop [80] using some elaborate machinery involving standardization and postponement of certain reductions. We show how an extension to the infinitary lambda calculus, where Böhm trees can be directly treated and rewritten as infinite terms, yields a simple and intuitive proof of the correctness of these Church-Rosser counterexamples. (2) In Barendregt [84] it is shown that Surjective Pairing is not definable in lambda calculus. We show how this result can easily be obtained as a corollary of Berry's Sequentiality Theorem, which itself can be proved by an excursion to the infinitary lambda calculus.
  • Kim Bruce: Modularity and Scope in Object-Oriented Languages
    [Abstract] Language designers for object-oriented languages have tended to use classes as the main modularity boundaries for code. While Java includes packages, they were not particularly well thought-out and have lots of flaws. However, the designers got very little flack for the weak design because programmers don't use them very effectively. In this talk we describe some useful properties of modularity and information-hiding mechanisms in object-oriented languages and and present a language design that supports these properties.
  • Luca Cardelli: Artificial Biochemistry
    [Abstract] Chemical and biochemical systems are presented as collectives of interacting stochastic automata: each automaton represents a molecule that undergoes state transitions. This framework constitutes an artificial biochemistry, where automata interact by the equivalent of the law of mass action. We analyze several example systems and networks, both by stochastic simulation and by ordinary differential equations.
  • Pierre-Louis Curien: Computational self-assembly
    [Abstract] The object of this talk is to appreciate the computational limits inherent in the combinatorics of the κ-calculus, an applied concurrent language originally meant as a visual and concise notation for biological signalling pathways. We define a compilation of κ into a language where interactions can involve at most two agents at a time. That compilation is generic, the blow-up in the number of rules is linear in the total rule set size, and the methodology used in deriving the compilation relies on an implicit causality analysis. The correctness proof is given in details, and correctness is spelt out in terms of the existence of a specific weak bisimulation. Allowing some of the rules to be reversible allows to avoid deadlocks.
  • Mariangiola Dezani : Session Types for Object-Oriented Languages
    [Abstract] A session takes place between two parties; after establishing a connection, We study the incorporation of session types into object-oriented languages through MOOSE, a multi-threaded language with session types, thread spawning, iterative and higher-order sessions. Our design aims to consistently integrate the object-oriented programming style and sessions, and to be able to treat various case studies from the literature. We describe the design of MOOSE, its syntax, operational semantics and type system, and develop a type inference system. We discuss also two extensions: subtyping with bounded quantification enhancing typeability and asynchronous communications enhancing progress. (Joint work with Alex Ahern, Mario Coppo, Sophia Drossopoulou, Elena Giachino, Dimitris Mostrous, and Nobuko Yoshida).
  • Abbas Edalat: Recursively measurable sets and computable measurable sets
    [Abstract] In 1950's, N. A. Sanin introduced the notion of a recursively measurable set of the real line with respect to the Lebesgue measure. It turned out to be equivalent to a similar notion that G. Kriesel and D. Lacombe had also developed. We have recently introduced the notion of computable measurable set with respect to any Borel measure on any locally compact second countable Hausdorff space. This new notion combines both set-theoretic and measure-theoretic approximations. A computable measurable set is approximated in the measure with a recursive sequence of basic open sets, each containing the original set, and a recursive sequence of basic closed sets, each contained in the original set. We show that a recursively measurable set can be constructed up to a null set as the limsup of its defining sequence of open sets. We then show that for the Lebesgue measure on the real line, where recursively measurable sets are defined, a computable measurable set is recursively measurable but not vice versa. We also compare the resulting notions of recursively measurable (Lebesgue integrable) functions and computable measurable (Lebesgue integrable) functions.
  • Jean-Yves Girard: Truth, modality, intersubjectivity
    [Abstract] Logic has so far been unable to cope with truth, witness Tarki's "definition". In a finite von Neumann algebra, e.g., the Murray-vN hyperfinite factor, truth can be defined w.r.t. a viewpoint, i.e., a maximal abelian subalgebra. The modality "necessary" appears as the affirmation of truth. Truth is therefore subjective, in the style of quantum measurement. This calls for an intersubjective explanation of logic.
  • Furio Honsell and Gordon Plotkin: On the βη-completeness and expressiveness of some classes of combinatory algebras
    [Abstract] The question whether there exists a Scot continuous retract model of βη is 25 years old, and still open! We discuss and solve several variations of this problem such as the βη-completeness and expressiveness of various classes of combinatory models for various classes of FOL formulae.
  • Eugenio Moggi: Category Theory and Lambda Calculus
    [Abstract] We give an overview of the category-theoretic view of models for the lambda calculus and related systems. Starting from the seminal idea of Scott (models of the untyped lambda-calculus as reflexive objects in a CCC), we review how models for other calculi (e.g. combinatory logic and second-order lambda calculus) have been described in Category Theory, and the role of Giuseppe Longo on these developments.
  • Mioara Mugur-Schächter: On the patient quest of Giuseppe Longo for a general unity and coherence
    [Abstract] In these times of utterly parcelling specialization, views stemming from a severe education of rigor and nevertheless rooted in a deep perception of the powers of intuition and a universal curiosity concerning the various forms of human thought, are extremely rare. Via two examples - of which one concerns the specificity of quantum mechanical probabilities with resect to classical ones and the question of determinism and the other one the relations between physics and biology - I shall argue that Giuseppe Longo is developing such a view.
  • Thierry Paul: Semiclassical analysis and sensitivity to initial data
    [Abstract] We will present several recent results concerning the transition between quantum and classical mechanics, in the situation where the underlying dynamical system has an hyperbolic behaviour. The special role of invariant manifolds will be emphasized, and the long time evolution will show how the quantum non-determinism and the classical chaotic sensitivity to initial conditions can be compared, and in a certain sense overlap. An analogy with computer sciences (numerical computation for partial differential equations) will also be discussed.
  • Jean Petitot: Neurogeometry and the origin of space.
    [Abstract] Recent experiments in neurophysiology enable to better understand the processing of visual inputs by cortical primary visual areas. Global properties of percepts, in the sense of Gestalt theory, are a consequence of the functional architecture of these areas. We have shown that the f unctional architecture of V1 implements the contact structure of the visual plane. This explains many properties of the integration of local sense data into global perceptual structures.
  • John Stewart: Is "life" computable?
    [Abstract] Robert Rosen has proposed a theoretical definition of "life itself" as "closure under efficient cause". He has further put forward the conjecture that a model of "life", so defined, is not computable. In this talk, I propose to present this conjecture, which is controversial (but which has important consequences for attempts to model "artificial life" in the computer); and to present also some recent developments which, although they do not entirely settle the controversy, represent a significant advance.

Thursday, June the 28th, 2007 - Amphitheater 3 (number 31 on this map)

14:00 – 14:10 Welcome
14:10 – 15:30 Session 1: Lessons from Logic and Physics
Mioara Mugur-Schächter:
On the patient quest of Giuseppe Longo for a general unity and coherence
Jean-Yves Girard:
Truth, modality, intersubjectivity
15:30 – 16:00 Coffee break
16:00 – 16:40 Session 2: Geometry and Cognition
Jean Petitot:
Neurogeometry and the origin of space
16:40 – 18:00 Session 3: Models and Categories
Eugenio Moggi:
Category Theory and Lambda Calculus
Martin Hyland:
Modelling the Impossible

Friday, June the 29th, 2007 - Amphitheater A (number 4 on this map)

09:00 – 10:20 Session 4: Lambda Calculus
Henk Barendregt and Jan Willem Klop:
Non-left linear reductions via infinitary lambda calculus
Furio Honsell and Gordon Plotkin:
On the βη-completeness and expressiveness of some classes of combinatory algebras
10:20 – 10:40 Coffee break
10:40 – 12:40 Session 5: Theoretical Biology and Biological Theories
Pierre-Louis Curien:
Computational self-assembly
Luca Cardelli:
Artificial Biochemistry
John Stewart:
Is "life" computable?
12:40 – 14:00 Symposium lunch (provided)
14:00 – 15:20 Session 6: Types for Object-Orientation
Mariangiola Dezani:
Session Types for Object-Oriented Languages
Kim Bruce:
Modularity and Scope in Object-Oriented Languages
15:20 – 15:40 Coffee break
15:40 – 17:00 Session 7: Analysis, Physics, and Recursion Theory
Abbas Edalat:
Recursively measurable sets and computable measurable sets
Thierry Paul:
Semiclassical analysis and sensitivity to initial data
17:00 – 17:50 Closing Talk
Giuseppe Longo:
From exact sciences to life phenomena: a few concluding remarks on Bohr and Schrödinger
Venue, Registration, and Organisation
Informations about the venue, travel, organization, and registration are to be found in the RDP 2007 page. The plan of the conference rooms is available here. Registration desk is located in the room "salle des textiles".
Page mantained by gc.