Longo Symposium

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.
Martin Hyland : Modelling the Impossible
[Abstract] Ideas which one cannot model naturally within classical set theoretic mathematics present both conceptual and technical challenges. Two important examples are the pure lambda calculus and the polymorphic lambda calculus. Giuseppe Longo has made important contributions to both areas. However though examples of models are known, very little in general is known about the equations satisfied in these models or about the relation between models. In this talk I shall discuss the range of models known for the two theories, and shall indicate how to find many more models. In the process I hope to impose some preliminary structure on the collection of models.
Giuseppe Longo : From exact sciences to life phenomena: a few concluding remarks on Bohr and Schrödinger
[Abstract] N. Bohr and E. Schrödinger wrote briefly and rather informally about life in their maturity. Their experience as authors, in different ways, of a theoretical divide between classical (or relativistic) Physics and microphysics lead them towards a similar autonomy of thought in Biology. We will try to learn from these extraordinary physicists the methodological lesson as well as few theoretical hints towards a systemic approach to life phenomena.
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)

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