« Constructivisme et extraction de programmes »

Rencontre de l'ACI GEOCAL

23--24 novembre 2004, à la Faculté des Sciences de Luminy





Le 25 novembre 2004, Per Martin-Löf (Stockholm) recevra le titre de Docteur Honoris Causa de l'Université de la Méditerranée.

À l'occasion de sa venue à Marseille, l'ACI GEOCAL organise une rencontre dont le thème général est « constructivisme et extraction de programmes ». Cette rencontre aura lieu sur le Campus de Luminy les deux jours précédant la remise officielle du titre de Docteur Honoris Causa à Per Martin-Löf.

Très informelle, cette rencontre consistera en une série d'exposés donnés par des orateurs invités dont les travaux ont, ou ont eu, des liens profonds avec les contributions fondamentales de Per Martin-Löf à la logique et à l'informatique théorique (intuitionisme, théorie des types...). Ces exposés porteront sur des sujets liés au constructivisme et à l'extraction de programme, mais pas uniquement. Notre motivation est bien moins l'homogénéité thématique que l'espoir de voir surgir des discussions (controverses ?) parmi l'auditoire et les orateurs.

L'organisation de cette rencontre a reçu le soutien actif de la Faculté des Sciences de Luminy, du Centre International de Rencontres Mathématiques et de l'Institut de Mathématiques de Luminy. Nous les en remercions chaleureusement.




Inscriptions

Envoyer un mail à Marie-Renée Fleury-Donnadieu : mrd[_AT_]iml.univ-mrs.fr, en précisant bien :




Lieu

La rencontre se tiendra à la Faculté des Sciences de Luminy, dans l'amphithéatre 12 (batiment 9 sur le plan suivant), et les repas seront pris au CIRM.

Pour se rendre à Luminy : le plus simple est de prendre le métro jusqu'au Rond-Point du Prado, puis le bus 21 (voir le site de la RTM et aussi Le Pilote).

NB: il y a aussi une version rapide du 21, le JETBUS, départ du Rond-Point du Prado, toutes les 15mn entre 7h20 et 9h30. Durée du trajet: 20mn. Retour vers le Rond-Point du Prado dans l'après-midi: toutes les 15mn entre 16h15 et 18h15. Utilisable avec les cartes de transport de la RTM (Solo qu'on peut acheter dans le bus, Double Solo ou Libertés).

Pour se rendre au CIRM : accès. Le CIRM correspond au numéro 12 (rouge) sur ce plan du campus de Luminy.




Hôtels

Chacun devra réserver son hôtel. On pourra consulter cette liste à cet effet.




Liste des orateurs




General program

small map
  • Tuesday:
    • 8'45--9'05: reception and coffe at the "Institut mathématique de Luminy" (IML), 3rd floor in room 310;
    • 9'15--12'15: talks in "amphithéatre 12" in building B (behind the IML building);
    • 12'15--14'00: lunch at the "Centre international de rencontres mathématiques" (CIRM), which lies on the right of the main road;
    • 14'00--15'30: talks in amphithéatre 12;
    • 15'30--16'00: coffe at the IML, room 310;
    • 16'00-17'30: last talks for the day, in amphithéatre 12.
  • Wednesday:
    • 9'00--9'20: reception and coffe at the "Institut mathématique de Luminy" (IML), 3rd floor in room 310;
    • 9'30--12'15: talks in "amphithéatre 12" in building B (behind the IML building);
    • 12'15--14'00: lunch at the "Centre international de rencontres mathématiques" (CIRM), which lies on the right of the main road;
    • 14'00--16'00: talks in amphithéatre 12;
    • 16'00--16'30: coffe at the IML, room 310;
    • 16'30-17'30: last talk for the day, in amphithéatre 12.



Programme provisoire

Mardi 23 novembre :

8'45--9'05 Accueil et café à l'Institut mathématique de Luminy, au troisième étage
9'15--9'30 Introduction et présentation dans l'amphithéatre 12, batiment 9
9'30--10'30 Per Martin-Löf: "Normalization by evaluation and by the method of computability"
10'30--10'45Break
10'45--11'30 Peter Hancock: "Programs and the real world"
11'30--12'15 Ulrich Berger: "A Semantic Strong Normalization Proof for Higher-Type Rewrite Systems"
12'15--14'00 Lunch
14'00--15'00 Martin Hofmann: "Non size increasing polytime computation: 5 years later"
15'00--15'30 Yves Bertot: "Type theory based descriptions of partial co-recursive functions"
15'30--16'00Break
16'00--16'30 Assia Mahboubi: "Quantifier elimination over real closed fields inside the Coq system"
16'30--17'30 Gerard Huet : « Des Lambdas et des Aums »


Mercredi 24 novembre :

9'00--9'20 Accueil et café à l'Institut mathématique de Luminy, au troisième étage
9'30--10'30 Jean-Louis Krivine: TBA
10'30--10'45Break
10'45--11'30 Alexandre Miquel: "A Strong Normalisation Theorem for Zermelo-Fraenkel Set Theory"
11'30--12'15 Gilles Dowek: "Axiom vs. computation rules: a state of the art"
12'15--14'00 Lunch
14'00--15'00 Thierry Coquand: "Elimination of choice sequences and commutative algebra"
15'00--16'00 Thomas Streicher: "A Type-Theoretic Reconstruction of Joyal and Moerdijk's Algebraic Set Theory"
16'00--16'30 Break
16'30--17'30 Jean-Yves Girard: "Clifford algebras and logic"
20'00Dinner


Jeudi 25 Novembre, matin : amphithéatre Herbrand (130--134, premier étage), à l'Institut mathématique de Luminy

10'00--11'00 Lutz Straßburger: "Naming proofs in classical propositional logic"
11'00--12'00 Paul-André Melliès: "Asynchronous games: an innocent model of linear logic"

Jeudi 25 novembre, 16h :

Journée académique et scientifique de de l'Université de la Méditerranée, à la Faculté de médecine, salle de conférence Maurice Toga, 27 boulevard Jean-Moulin, 13385 Marseille, métro Timone. Le programme de la cérémonie officielle, au cours de laquelle Per Martin-Löf recevra le Doctorat Honoris Causa, se trouve ici. La remise des titres de Docteur Honoris Causa aura lieu à 18h.



Organisateurs

La rencontre est organisée par Thomas Ehrhard, Marie-Renée Fleury-Donnadieu et Pierre Hyvernat.

Pour toute question concernant la rencontre, vous pouvez envoyer un email à Marie-Renée Fleury-Donnadieu (mrd[_AT_]iml.univ-mrs.fr) ou à Pierre Hyvernat (hyvernat[_AT_]iml.univ-mrs.fr).




Résumés

Peter Hancock

Programs and the real world.
I first learnt about type theory and something about programming from Per. After a few years I was employed writing programs to monitor and control various (usually dangerous) things: scientific experiments on human hearing, heavy machinery, computer systems running user programs, and transactions involving bank accounts. It has not always been easy to reconcile theory with practice. I shall present some resulting ideas about programs, programming, constructive mathematics, and applying mathematics in the physical (or in any sense "real") world.

Ulrich Berger

A Semantic Strong Normalization Proof for Higher-Type Rewrite Systems.
We consider the untyped lambda calculus with constructors and recursively defined constants. We define the n-th approximation of a term M as the term M_n obtained by replacing every constant c with a constant c_n which is defined like c except that it unfolds only n times. We show that if M does not denote bottom in a suitable strict domain-theoretic model and all M_n are strongly normalizing, then M is strongly normalizing. We transfer this result to typed lambda calculi extended by various forms of transfinite- and bar-recursion in higher types for which strong normalization was hitherto unknown. The motivation for this work comes from computational problems arising in connection with program extraction from classical proofs.

Martin Hofmann

Non size increasing polytime computation: 5 years later.
In 1999 I have proposed an extension of multiplicative linear logic with a new type <> and inductive datatypes where each constructor takes an extra argument of type <>. For example, unary natural numbers are a type N and come with constants 0:N and S:<> -o N -o N and an iteration principle: from closed terms z:A and s:<> -o A -o A derive It(z,s):N -o A. There are no closed terms of type <>.
It was shown that all functions on lists of booleans definable in this system are non-size increasing (length of f(l) <= length(l)) and polytime computable. Later in 2002 I was able to show that all non size-increasing polytime functions are definable in the system, in particular all characteristic functions of problems in P.
One (arguable) deficiency of the system is that data types are primitive concepts and not definable via impredicative encodings as is done in systems like Light or Soft Linear Logic (LLL, SLL). On the other hand, concrete programming is much easier in my system than in those systems.
Over the last two years I attempted to extend my system with impredicative quantification and a !-modality so as to allow for impredicative encodings of data types and better comparison with LLL, SLL. Doing so is surprisingly difficult but some partial results begin to emerge.
The talk will recall the existing results on non size-increasing computation and also discuss the recent advances.

Yves Bertot

Type theory based descriptions of partial co-recursive functions.
Techniques have been proposed recently to describe partial recursive functions in type theory with inductive types. We study an extension of these techniques to co-recursive functions and show how that they fit in frameworks that accepted guarded co-recursive definitions. We give an example with filters on streams and Eratosthene's sieve.

Assia Mahboubi

Quantifier elimination over real closed fields inside the Coq system
It is known since the work of Tarski in 1948 that one can perform quantifier elimination in the theory of a real closed field. This result has fundamental consequences in real algebraic geomerty. In particular it is possible to build a decision procedure to decide whether a polynomial system with rational coefficients has a real solution or not. We will explain how to design such a decision procedure inside the Coq system, relying on the cylindrical algebraic decomposition, which is a more recent (Collins 1966) and a more efficient method than Tarski's historical one.

Gilles Dowek

Axiom vs. computation rules: a state of the art.
In the history of logic, several formalisms have proposed to replace axioms by compuation rules. I will review some of them, trying to show that this idea was independently proposed in several contexts. I will then discuss the following open question: in predicate logic can we always replace axioms by computation rules.

Thierry Coquand

Elimination of choice sequences and commutative algebra.
The introduction of "Notes on Constructive Mathematics" (which presents the thesis work of Per Martin-Löf) contains a clear explanation of how Brouwer's bar theorem can be formulated in constructive mathematics. After presenting this explanation in the case of the fan theorem (compactness of Cantor space), we indicate how the same principle can be used in commutative algebra. One can in this way simplify the proofs of basic theorems (``Splitting off'' theorem of Serre, Bass stable range theorem, as formulated by Heitmann). In one case, the simplification is significant enough to suggest an improved version of the theorem (Forster-Swan's theorem).

Thomas Streicher

A Type-Theoretic Reconstruction of Joyal and Moerdijk's Algebraic Set Theory (and a Model of CZF+Sep where Every Set is Subcountable).
We show how Joyal and Moerdijk's purely categorical construction of initial Zermelo-Fraenkel algebras can be rephrased in a type theoretic fashion. It boils down to a modification of the "Aczel construction" showing that for a universe U (in the sense of Martin-Loef) the type V = (W A:U) A gives rise to a model of CZF. For showing that V validates Strong Collection and Subset Collection Aczel intrinsically employed the choice principles ensured by Martin-Loef type theory. Our construction deviates from Aczel's in the following respects:

  1. propositions are not interpreted as elements of U but instead as elements of a type Prop of *proof-irrelevant* propositions
  2. Prop may be assumed as impredicative, i.e. closed under arbitrary products.
As propositions are now proof-irrelevant AC is not for free anymore. To overcome this problem Joyal and Moerdijk have introduced a kind of type theoretic collection axiom (ttCA) saying that for any surjective e : X -->> A with A in U there exists a map f : C -> X with C in U and $e \circ f$ still surjective. An alternative to ttCA is the Projective Cover Axiom (PCA) saying that every type A in U can be covered by a projective object C (i.e. a C for which choice holds) in U. Whereas ttCA holds in Grothendieck and realizability toposes the simpler axiom PCA holds only in realizability toposes.
If Prop is an element of U then our modification of the Aczel construction gives rise to models of IZF. However, if U is interpreted as the modest sets over K_1 (the first Kleene algebra) and Prop as the assembly of proof-irrelevant modest sets then V = (W A:U) A gives rise to a model of CZF with full separation where every set is subcountable and which, therefore, refutes the power set axiom.
From work of Rathjen it is known that CZF+Sep has the strength of Second Order Arithmetic. Of course, one might like to construct models of CZF (without restricting the metatheory to be predicative) which also refute unbounded separation. This, however, seems to be hard because we don't know of any (non-term) models of type theory with a universe and a predicative type Prop.

Lutz Straßburger

Naming proofs in classical propositional logic
We present a theory of proof denotations in classical propositional logic. The abstract definition is in terms of a semiring of weights, and two concrete instances are explored. With the Boolean semiring we get a theory of classical proof nets, with a geometric correctness criterion, a sequentialization theorem, and a strongly normalizing cut-elimination procedure. With the semiring of natural numbers, we obtain a sound semantics for classical logic, in which fewer proofs are identified. Though a ``real'' sequentialization theorem is missing, these proof nets have a grip on complexity issues. In both cases the cut elimination procedure is closely related to its equivalent in the calculus of structures, and we get ``Boolean'' categories which are not posets.

Paul-André Melliès

Asynchronous games: an innocent model of linear logic.
Since its early days, deterministic sequential game semantics has been limited to linear or polarized fragments of linear logic. Every attempt to extend the semantics to full propositional linear logic has bumped against the so-called Blass problem, which indicates (misleadingly) that a category of sequential games cannot be self-dual and cartesian at the same time. We circumvent this problem here by considering
(1) that sequential games are inherently positional;
(2) that they admit internal positions as well as external positions.
We construct in this way an innocent model of propositional linear logic, which incorporates the well-bracketed and the non well-bracketed variants of the original arena game model by Hyland, Ong and Nickau.