Preuves, Programmes et Systèmes

Berline Meeting

Le planning du colloque ici : http://www.pps.jussieu.fr/berline-meeting/programme.

ABSTRACTS/RESUMES

Jean-Pierre Ressayre.

TBA

Stefano Berardi.

Beta-eta complete models and decompilers for system F. A decompiler is a map extracting a code for a program out of the extensional behaviour of the program itself. A model is beta-eta complete if its equational theory is beta-eta. We define a model of system F inside system F itself, and a ecompiler for this "internal" model. We derive as a consequence the fact that inside any model of system F we may define a beta-eta complete model of system F.

Antonino Salibra.

Non-effective theories of effective models of lambda calculus.

Klaus Grue.

Map theory: From syntax to models and back.

Map Theory (MT) is a theory which comprises lambda calculus extended by a quantifier. MT can do anything that set theory can do, and it fulfills Alonzo Church's original goal to be able to base all of mathematics on lambda calculus.

The original version of Map Theory (MT) had complicated axioms and an over-complicated model. This situation was enhanced greatly when Chantal Berline and I managed to establish a "kappa-model" based on kappa-continuous functions. The kappa-model satisfied all axioms of the original MT, thus proving consistency.

It turned out, however, that the kappa-model had more to offer: the insight gained from the kappa-model has allowed to simplify the syntactic formulation of MT dramatically.

The talk presents on-going joint work between Chantal Berline and me. The talk focuses on the syntax, axioms, inference rules, and applications of the simplified MT.

Thomas Ehrhard.

Le modèle de Scott est le collapse extensionnel du modèle des ensembles et des relations.

Le modèle relationnel de la logique linéaire est peut-être le plus simple, mais il induit une catégorie cartésienne fermée qui « n'a pas assez de points », c'est-à -dire que le simple comportement applicatif des morphismes ne suffit pas à les caractériser. C'est dû au fait que l'exponentielle est interprétée au moyen de multi-ensembles finis (en essayant avec des ensembles finis à la place, on n'obtient pas un modèle). On montrera qu'en identifiant héréditairement les morphismes selon leur comportement applicatif ­— c'est l'opération de collapse extensionnel — on obtient le modèle des treillis complets premier-agébriques et fonctions Scott-continues. Toutes les constructions requises seront faites dans un cadre strictement linéaire (la sémantique de Scott est une sémantique de la logique linéaire).

Bruno Poizat.

La vie et l'oeuvre de Chantal Berline.

Je rappellerai la contribution de Berline a l'etude des parties generiques des groupes stables, et je montrerai comment on peut retrouver les resultats de Cherlin sur les groupes de petits rang de Morley dans le contexte plus acrobatique du rang de Cantor, ou justement les ensembles generiques sont plus difficiles a manier que dans le cas stable.

Carol Wood.

The Joy of Examples.

I will describe the role of certain examples in model theory, including ones inspired by Berline's work.

Gregory Cherlin.

Between model theory and combinatorics: Homogeneity, WQO, Universality.

I will discuss some problems in and around graph theory which are connected with the study of homogeneous structures: the classification of distance homogenous graphs (graphs which are homogeneous when considered as metric spaces in the graph metric); recoginition of wqo classes of combinatorial structures determined by finitely many forbidden substructures; and (if time permits) the problem of the existence of a countable universal graph within the class of graphs omitting a finite set of forbidden subgraphs. The last two problems are decision problems, the question being whether there are algorithms which recoginizes the favorable cases, with the finite constraint set as input.

Francoise Delon.

Différentes notions de théories minimales.

Chantal Berline.

The universe "is" a lambda-term.

The Map Theory of Klaus Grue fulfills the Church's original intention of finding a foundation that would work simultaneously for the mathematics and for the computation theory and that is based on the notion of functions and application rather than the notion of sets and the membership relation. In this talk we will give indications on the nature/construction of the canonical model MCAN of Map theory, using an inaccessible cardinal sigma (and a regular cardinal kappa above it). MCAN is, to begin with, a topological model of lambda-calculus, that is, a universe of continuous maps that can be applied to themselves. MCAN also has a notion of well-founded maps, which form an open subset PHI of MCAN, in correspondance with the universe V_sigma of well-founded sets. It can be proved that PHI is definable by a lambda-term(more accurately: that its characteristic function is the interpretation of an MT-term). This is the base of the new axiomatisation MT of Map theory, which essentially gets rid of all the construction axioms of the original MT, and is the most difficult part of its consistency proof. This is on-going joint work with Klaus Grue.