Archives du séminaire de Logique, Lambda-calcul et Programmation.
98/99 (Responsables : V. Danos, C. Berline, J.L. Krivine, P. Rozière).


30/10/98: Jean-Louis Krivine (Paris 7) Lambda-calcul typé dans ZF.

6/11/98: Jean-Yves Girard (IML Marseille) Introduction à la ludique.

27/11/98: Thomas Ehrhard (IML Marseille) Sur les rapports entre définissabilité et prouvabilité dans MALL (travail en collaboration avec Antonio Bucciarelli).

4/12/98: double séance :
10h30: Tristan Crolard (Paris 7) Un lambda-calcul typé avec coroutines.
11h30: Juliusz Chroboczec (Université d'Édimbourg) Un lambda-calcul avec erreurs et sous-typage. résumé

18/12/98: Klaus Grue (Université de Copenhague) Dedekind cuts as a means for constructing kappa-Scott domains. abstract

15/01/99: Simone Martini (Université d'Udine) Local reductions in box-free proof-nets.

5/02/99: Paul Ruet (Université d'Edimbourg) Modeles de la logique lineaire non-commutative.

12/02/99: Jayanta Sen (University of Calcutta) Embedding Lukasiewicz aleph_0 logic in Linear Logic : an algebraic approach.

5/03/99: Andreja Prijatelj (Université de Ljubljana) From bounded structural rules towards linear modalities.

12/03/99: Serge Grigorieff (UFR d'informatique Paris 7 et Laboratoire de Logique, Algorithmique, Informatique de Clermont 1) Prédicats de vérité syntaxique pour l'arithmétique du second ordre (travail avec Loïc Colson).

26/03/99: Jean Goubault (Dyade, Rocquencourt) Encore un calcul du premier ordre pour le lambda-calcul. résumé

2/04/99: Christophe Raffalli (Université de Chambéry) Synthèse de types dans le système F.
Présentation d'un semi-algorithme complet et efficace pour le système F.

9/04/99: double séance:
10h30: Jean-François Monin (CNET Lannion) Vérification formelle d'un algorithme normalisé de contrôle de conformité ATM : bilan de quelques expériences et perspectives pour les méthodes formelles résumé
11h30: Pascal Brisset (CNET Lannion) Sécurité des architectures à code mobile : vers un vérifieur de byte-code Java certifié ; code auto-certifié ("Proof-Carrying Code").

16/04/99: Vincent van Oostrom (CWI et Utrecht University) Normalization in weakly orthogonal rewriting. abstract

23/04/99: pas de séance

30/04/99: pas de séance

7/05/99: Patrick Baillot (Marseille) Complexité élémentaire et géométrie de l'interaction (travail en collaboration avec Marco Pedicini) résumé

l'exposé de John Longley est reporté au lundi 17 mai à 10h salle 401, 45-46.

17/05/99: John Longley (Edinburgh) The Sequentially Realizable Functionals or When is a functional program not a functional program? abstract
salle 401, 45-46, 10h.

21/05/99: Pas de séance

28/05/99: René David (Chambéry) Tout lambda terme non resoluble admet une decoration. résumé

4/06/99: Abbas Edalat (London, Imperial College) Foundation of a Computable Solid Modeling (work with Andre Lieutier, Scientific team, Matra Datavision & XAOLAB, LIM, Marseilles). abstract

11/06/99: Paul André Mellies (Paris 7) PAM Concurrent Games and Full Completeness for MALL.

18/06/99: Russ Harmer Games Semantics for Finite Non-determinism.

25/06/99: Vincent Danos calcul des séquents et continuations.


Archives du séminaire de Logique, Lambda-calcul et Programmation.
97/98



3/10/97: Alessandra Carbone (Paris 12) Un modèle combinatoire de l'élimination des coupures.
10/10/97: Vincent Danos (Paris 7) Logique Linéaire et temps polynomial (d'après Girard, Asperti).
17/10/97: Jean-Louis Krivine (Paris 7) Théorème de complétude (suite).
24/10/97: pas de séance
31/10/97: Vincent Danos (Paris 7) Modèles de jeux et modèles usuels.
7/11/97: Francois Fages (ENS) Sémantique des phases et preuve de sûreté des programmes concurrents avec contraintes.
14/11/97: Matthias Baaz (Vienne, Autriche) Generalization and the introduction of cuts.
21/11/97: Lorenzo Tortora de Falco (Rome) Caractérisation sémantique de l'équivalence des réseaux.
28/11/97: Ying Jiang (Paris 7, Académie des sciences de Chine) Réalisabilité des formules universelles du système F.
5/12/97: Antonio Bucciarelli (Rome, "la Sapienza") Logical Relations and definability in simple types.
12/12/97: Stefano Berardi (Turin) Modèles complets du système F.
19/12/97: Jean Goubault (Dyade, Rocquencourt) Connaissance cryptographique et élimination des coupures.
16/1/98: double séance
10.30: Pasquale Malacaria (London, Imperial College) Static analysis of programs via games.
11.30: Russel Harmer (London, Imperial College) Games & non-determinism.
23/1/98: double séance
10.30 Martin Hyland (Cambridge) Categories of Games.
11.30: Jean-Yves Girard (IML, Marseille) On the meaning of logical rules.
30/1/98: Nuno Barreiro (Lisbonne) Sur le collapse extensionnel de la semantique coherente multiensembliste.
27/2/98: Olivier Bastonero (Turin, Paris 7) Une classe de modèles du lambda calcul paresseux
6/3/98: Benedetto Intriguila (Rome) Extension of Kruskal's Theorem to Rational Trees
13/3/98: Abbas Edalat (London, Imperial College) Exact real arithmetic by domain theoretic methods
Simona Ronchi della Rocca (Turin) Call-by-value solvability
20/3/98: Samuel Lacas (Paris 7) Axiome du choix au second ordre
27/3/98: Philippe Codognet (INRIA, Sony) Contraintes sur les domaines finis en Programmation Logique avec Contraintes: compilation et extensions.
3/4/98: Tristan Crolard (Paris 7) Dualité en logique intuitionniste du second ordre
10/4/98: pas de séance
17/4/98: Andre Scedrov (Penn, Philadelphie) Specifying Real-Time Finite-State Systems in Linear Logic
24/4/98: Guy Cousineau (Paris 7) Programmation fonctionnelle graphique
29/4/98: Tobias Nipkow (Munich) Java-light is Type Safe
15/5/98: Alain Prouté (Paris 7) Topos et programmation
29/5/98: Furio Honsell (Udine) Theories et Modeles du lambda-calcul
Marina Lenisa (Udine) Semantique finale
26/6/98: Chantal Berline (Paris 7) Des modeles simples pour le Systeme F
3/7/98: Mohamed Mezghiche (Tizi Ouzou) C beta-reduction et evaluation partielle des lambda-expressions

Archives du séminaire de Logique, Lambda-calcul et Programmation.
96/97



27/9/96: Luke Ong (Cambridge) Lambda-mu calculus, syntax and semantics
4/10/96: Pierre-Louis Curien (ENS) Algorithmes séquentiels et Jeux
11/10/96: Thierry Joly (Paris 7) Variations sur le théorème de Böhm
25/10/96: Gerard Huet (INRIA) Arbres de Böhm rationnels
1/11/96: Relâche
8/11/96: Karin Horwein (Vienne) Structuring of (LK-)proofs by quantifier distribution
15/11/96: Cédric Fournet (INRIA) Join Calculus: un calcul pour agents mobiles
22/11/96: Gérard Boudol (INRIA Sophia) Une synthèse des programmes fonctionnels et concurrents
29/11/96: Hugo Herbelin (Paris 10) Sémantique de Jeux pour PCF classique
6/12/96: Olivier Bastonero (Paris 7) Sémantique fortement stable et résultats d'incomplétude
13/12/96: Simona Ronchi della Rocca (Turin) The operational content of intersection types
20/12/96: Sophie Malecki (Nancy) F3 et Fomega
27/12/96 et 3/1/97: Relâche
10/1/97: Peter Selinger (Penn Philadelphia) Modèles finis du lambda-calcul
17/1/97: Arnaud Fleury (Paris 7) Logique linéaire multiplicative tressée
24/1/97: Christophe Raffalli (Paris 12) Le théorème de mise en mémoire pour tous les types
31/1/97: Yves Lafont (Marseille, IML) Problèmes de décision en logique linéaire
31/1/97: Jean-Yves Girard (Marseille, IML) Fragments d'une Sémantique
31/1/97: Thomas Ehrhard (Marseille, IML) Jeux, espaces cohérents contractiles et hypercohérences
7/2/97: Elias Tahhan Bittar (Clt-Ferrand) Normalisation forte pour des calculs de séquents
7/2/97: Max Kanovich (Russian State Univ., Moscou) Phase semantics for light linear logic
14 et 21/2/97: Relâche
28/2/97: Jean Goubault (INRIA Rocquencourt, Bull) Quote, eval et l'isomorphisme de Curry-Howard pour S4
7/3/97: Jean-Louis Krivine (Paris 7) A propos du second théorème d'incomplétude
14/3/97: Thierry Coquand (Göteborg) Analyse du théorème de Van der Waerden
21/3/97: Relâche
28/3/97: François Métayer (Paris 10) A propos de la règle d'échange
4/4/97: Vincent Danos (Paris 7) Logique linéaire et jeux
11 et 18/4/97: Relâche
25/4/97: Hugo Herbelin (Paris 10) Arités et évaluation dans le système F
25/4/97: Christian Rétoré (CRIN/INRIA) Sémantique cohérente et réseaux multiplicatifs
2/5/97: Peter Clote (Munich) Cutting planes
9/5/97: Relâche
16/5/97: François Métayer (Paris 10) Géométrie de la réécriture
23/5/97: Lorenzo T. di Falco (Paris 7/Rome) Isomorphismes calculatoires en logique classique
30/5/97: Samuel Lacas (Paris 7) L'axiome du choix et le tiers exclus dans ZF
6/6/97: Denis Bechet (CRIN/INRIA) Minimalité du critère de correction des réseaux de preuve multiplicatifs
13/6/97: Relâche
20/06/97: Edouard Dorard (Paris 7) Jeux additifs (d'après Joyal)
27/06/97: Alberto Pravato (Université de Turin) Categorical models of untyped lambda-calculi: a monoidal approach

Archives du séminaire de Logique, Lambda-calcul et Programmation.
95/96



7/4/96 Myriam Quatrini (LMD Marseille) Sémantique cohérente des exponentielles
14/4/96 Pierre-Louis Curien (CNRS-ENS) Séquentialité et jeux
5/5/96 Hugo Herbelin (LITP Paris7) Calcul des séquents et jeux, application au lambda-calcul
12/5/96 Gilles Dowek (INRIA-Rocquencourt) Collections, types et ensembles
19/5/96 Vincent Danos (CNRS-Paris 7) Machines réversibles, irréversibles et optimales pour le lambda-calcul
2/6/96 Vincent Padovani (Paris 7) Le filtrage atomique est décidable
9/6/96 Yves Lafont (LMD Marseille) Problèmes de décision en logique linéaire et sémantique des phases
14/6/96 Simon Gay (Royal Holloway-LIX) Interaction categories: a theory of types for concurrency
21/6/96 Benjamin Werner (INRIA) Théorie des ensembles en théorie des types
28/6/96 Ian Mackie (LIX) Parallel interaction nets