Extraction de programmes à partir de preuves classiques
en Coq,
PDF,
4 pages/1.Exposé donné au séminaire du VERIMAG (Grenoble). (Version courte de l'exposé donné au LIX, avec quelques ajouts.) Avril 2009.
Extraction de programmes à partir de preuves classiques
en Coq,
PDF,
4 pages/1.
Exposé donné au séminaire du VERIMAG (Grenoble).
(Version courte de l'exposé donné au LIX, avec
quelques ajouts.)
Avril 2009.
Extraction de programmes à partir de preuves classiques
en Coq,
PDF,
4 pages/1.
Double exposé (2 × 2h) donné au séminaire du LIX.
(Version longue et plus aboutie de l'exposé donné
à Lyon.)
Avril 2009.
Extraction de programmes à partir de preuves classiques
en Coq,
PDF,
4 pages/1.
Exposé donné au séminaire commun Plume/LIMD à Lyon.
Février 2009.
Construction de programmes à partir
de preuves non constructives,
PDF,
4 pages/1.
Exposé donné lors des Journées nationales du GDR-IM.
Janvier 2009.
Extraction de programme classique dans le calcul des constructions,
PDF.
Exposé donné dans le cadre du séminaire LogiCal/Proval (LIX)
Février 2008.
Une introduction à la réalisabilité,
PDF,
4 pages/1.
Présentation de la
réalisabilité intuitionniste (Kleene)
et de la réalisabilité classique (Krivine).
Octobre 2007
La raisonnable efficacité des mathématiques
dans les sciences expérimentales,
PDF.
Exposé donné lors de la
Fête de la Science.
Octobre 2007
L'effectivité expérimentale des
mathématiques,
PDF.
Exposé donné au séminaire des thésards
PPS-LIAFA. Mars 2007
A lambda-calculus avec constructeurs,
PDF.
Avec Ariel Arbiser et Alejandro Ríos (UBA).
Une présentation (en anglais) du lambda-calcul avec constructeurs
présenté à RTA'06. Août 2006.
Vers des logiciels sans erreurs,
PDF.
Avec Pierre Moro (LIAFA).
Conférence donnée dans le cadre de la Fête de la Science.
Octobre 2005.
Réalisabilité et extraction de programmes,
PDF.
Exposé introductif donné dans le cadre du séminaire des thésards
LIAFA/PPS. Mars 2005.
A Strong Normalisation Theorem for Zermelo-Fraenkel Set Theory,
PS gzippé.
La version « classique »
du théorème de normalisation pour la
théorie des ensembles.
Exposé donné dans le cadre de la rencontre de
l'ACI GEOCAL
« Constructivisme
et extraction de programmes »
à l'occasion de la remise du diplôme de
docteur honoris causa de l'Université de la
Méditerranée (Aix-Marseille II)
à Per Martin-Löf.
Novembre 2004.
A Strongly Normalising Curry-Howard Correspondence for IZF
Set Theory,
PS gzippé.
Exposé donné à l'université Keio (Tokyo) lors du colloque
Proof Theory and its Applications. Mars 2004.
Un théorème de normalisation forte pour ZF intuitionniste (IZF),
PS gzippé.
Le même exposé, traduit en français, présenté au séminaire du
LAMA à Chambéry. Avril 2004.
Il s'agit d'une série de cinq cours (dits « intensifs ») que j'ai donnés au département d'informatique de l'Institut Technologique Chalmers (Göteborg, Suède) au début du mois de mars 2003 auprès d'un petit groupe d'étudiants de 3e cycle.
Cours no1:
An Introduction to System F,
PS gzippé,
PDF.
Cours no2:
The Strong Normalisation Theorem,
PS gzippé,
PDF.
Cours no3:
Normalisation of Second-Order Arithmetic,
PS gzippé,
PDF.
Cours no4:
Higher-Order Logic,
PS gzippé,
PDF.
Cours no5:
Inconsistent Type Systems
Désolé, pas de transparents pour ce cours (because flemme);
j'ai tout fait au tableau.
Il s'agit d'une série de trois cours que j'ai donnés lors de l'école d'été Proofs as Programs Paradigm qui a eu lieu à Eugene (Oregon, USA) au tout début de l'été 2002.
Cours no1: The Boolean Model of Type Theory,
PS gzippé,
PDF.
Cours no2: Encoding Zermelo's Set Theory into
System F-omega with Universes,
PS gzippé.
Cours no3: Curry-style Type Systems.
Désolé, pas de transparents pour ce cours (déjà because
flemme); j'ai tout fait au tableau.
Types in Coherence Spaces II,
PS gzippé.
Les deux premières parties d'un exposé en trois séances présenté au
séminaire ProgLog à Chalmers (Göteborg, Suède) en août 2002. Une
version plus pédagogique et plus aboutie de l'exposé de Lyon 2001,
centrée sur le système F-eta-inter. Malheureusement, la question des
types n'est abordée que dans la troisième partie de l'exposé, dont les
transparents se sont sans doute égarés au cours d'un
déménagement...
Types in Coherence Spaces I,
PS gzippé.
Exposé (de 20 minutes!) présenté dans le cadre de la session de
Logique du 1er congrès franco-américain de mathématiques (co-organisé
AMS-SMF), Lyon. Juin 2001.
Modèle d'un Calcul des Constructions avec univers, types
intersection et sous-typage dans les espaces cohérents.
PS gzippé.
Exposé présenté au séminaire de l'équipe Logique de la Programmation
(LDP) à l'Institut de Mathématiques de Luminy (IML), Marseille.
Janvier 2001.
Russell's Paradox in System U- (en anglais).
PS gzippé.
Exposé présenté au workshop TYPES'00 à Durham (G.-B.).
Décembre 2000.
Sémantiques dénotationnelles du Calcul des Constructions.
PS gzippé.
Exposé présenté au séminaire du projet Lemme/Prémisse à l'INRIA
Sophia-Antipolis.