LOGIQUE DE LA PROGRAMMATION

Organisatrice : Marie-Renée Fleury-Donnadieu  (téléphone : 04 91 26 96 38).
Lieu : Salle de Séminaire de l'IML, Bâtiment TPR2- CNRS, 3ème étage.

• Mardi 30 Novembre  1999 , 14h30  , Salle de Séminaire - 3ème étage.

• Vincent DANOS  et  Russ HARMER (CNRS- Paris VII)
                 1) Préliminaires de sémantique des jeux
              2) semantique des jeux probabilistes

• Mardi 19 Octobre 1999

• 10h , Salle de DEA - 2ème étage,    Rick BLUTE (University of Ottawa).
        Hopf Algebras and non-commutative logic.
 
• 14h30 , Salle de séminaire - 3ème étage : Mitsu OKADA (Keio University, visiting IML, Marseille).
        Some analysis on predicativity and impredicativity in phase model constructions.
 
Résumé : We analyze two impredicative constructions of phase models, one for intuitionistic phase model constructions, the other for higher order (but, of course, non-standard) phase model constructions.
(1)As for the former, we give a way to eliminate the usual impredicative constructions (of Abrusci, Troelstra, Ono et al.) of intuitionistic phase models and give a phase model construction with the help of the biorthogonality (double-nagation) of an extended (hidden) classical model: one consequence among others from this is that intuitionistic linear logic is complete with respest to the quasi-classical phase models. Here, a quasi-classical model is an intuitionistic model (M, Cl(*)) in which every intuitionistic fact Cl(X) is expressed by Cl(X)=X^{\bot,\bot} (it looks just a classical fact!), where \bot is the bottom of some classical model (M', \bot) for a monoid extension M' of M.
(2)As for the second, we analyze the nature of impredicativity and of non-standardness of the higher order phase-models construction, and we relate it to a (strongly) uniform phase-semantic higher order cut-elimination proof, which works not only for linear logic but also for all reasonable higher order logics uniformly. We also give some relationships between the linear logic proof-search method and some phase-semantic model constructions, (and give their application to a concurrent process calculus).
The first part of this work is on-going work with my Ph.D student, Kazushige Terui, and Max Kanovitch.
 
 
• Mardi 12 Octobre 1999 : JOURNEE LOGIQUE NON-COMMUTATIVE.

• 9h - 10h30        : Introduction.
• 11h-12h30        : Focalisation.
• 14h - 15h          : Connecteurs multiplicatifs généralisés.
• 15h - 15h45      : Modules.
• 15h45 - 16h30   : Réseaux.
 
• Vendredi 24 Septembre 1999, 10h , Salle de DEA, 2ème étage :

• Pawel URZYCZYN (Institute of Informatics, University of Warsaw).

Geometry of Insulation.
 
Résumé : Suppose that a polymorphic type $\sigma$ is embedded into another type $\tau$ by means of a (beta) left-invertible term $F:\sigma\to\tau$. We prove that $\sigma$ must be of height at most equal to the height of~$\tau$. It follows that recursive types equipped with the operators {\tt Fold\/} and {\tt Unfold\/} cannot be defined within the polymorphic lambda-calculus (System {\bf F}).
The proof of the above result is based on ideas borrowed from Geometry of Interaction and the theory of optimal reductions, namely it is an application of the regular/legal path technique to polymorphic terms.
 
 
• Jeudi 16 et Vendredi 17 Septembre 1999 : JOURNEES DE RENTREE,

particulièrement destinées aux étudiants nouveaux et anciens, animées par
J.-Y. Girard et Thomas Ehrhard.
 
• Jeudi 17 Septembre :
• 9h45 - 12h15 : Cours de J.-Y. Girard
• 14h30 - 17h : Suite

• Vendredi 18 Septembre :
• 9h45 - 12h15 : Cours de Thomas Ehrhard.
• 14h30 - 17h : Discussions
 
 
• Mercredi 23 Juin 1999, 14h30 , Salle de séminaire - 3ème étage.

 
• Giovanni PANI (Dipartimento di Informatica, Bari, Italie).

Direct and satisfactory strategies for games.

• Mardi 15 Juin 1999, 14h30 , Salle de séminaire - 3ème étage.

 
• : Philip J. SCOTT (Department of Mathematics, Ottawa, Canada).

Normalization and the Yoneda Embedding.

Résumé : We show how to solve the word problem for simply typed lambda calculus and various lambda theories, using elementary properties of presheaves and Yoneda embeddings (suitably per-enriched). This allows us to give a model-theoretic extraction of a normal form algorithm (yielding long beta-eta normal forms) without any use of traditional proof- theory or rewriting techniques. The methods are analogous to the Joyal-Gordon-Power-Street techniques for proving coherence in various structured bicategories as well as work of Berger-Schwichtenberg (LICS'91).

• Mardi 9 Mars 1999, 14h  , Salle de séminaire - 3ème étage.

• Roberto DI COSMO (ENS-Paris).

Réécriture dans les réseaux modulo équivalence structurelle.

Résumé : On s'intéresse à une version des réseaux de preuves avec contraction binaire qui est rendue libre de bouger par des règles d'équivalence structurelle justifiées par le calcul des séquents. En utilisant les résultats de Danos-Regnier (The Hilbert Space), nous prouverons que la réduction sur les classes d'équivalence des réseaux typés est encore fortement normalisante.
 
 
• Vendredi 22 Janvier 1999 , Salle de séminaire - 3ème étage.

 
• 9h30 - 10h30 : P.-L. CURIEN (ENS-Paris).
            Bistructures de cohérence.
 
• 11h - 12h : J.-L. KRIVINE (Paris VII).
            Lambda-calcul typé dans ZF.

Page Seminaire