Alexandre Miquel

Je suis maître de conférences (HDR) en informatique, actuellement en détachement au LIP à l'ENS Lyon dans l'équipe Plume.

Mon activité de recherche se situe à la frontière de l'informatique théorique et de la logique, et porte sur les liens qui unissent la démonstration mathématique et la programmation (essentiellement fonctionnelle) à travers la correspondance dite de Curry-Howard. Au sein de cette thématique, mes principaux centres d'intérêts sont:

• La logique (classique, intuitionniste, linéaire) et la théorie de la démonstration (normalisation, élimination des coupures).
• Les systèmes de types en général, qu'il s'agisse des systèmes de types à l'anglaise (polymorphisme à la ML), à la française (polymorphisme à la système F, calcul des constructions), à l'italienne (systèmes de types à la Curry, types intersection) ou à la suédoise (types dépendants, théorie des types de Martin-Löf).
• La sémantique (surtout dénotationnelle) des preuves et des programmes, et notamment la sémantique du sous-typage dans les espaces cohérents.
• La réalisabilité, notamment en théorie des ensembles (intuitionniste et classique).
• La démonstration assistée par ordinateur.

Lectures on classical realizability, LI2012: Lecture 1, Lecture 2.

J'ai soutenu mon habilitation à diriger des recherches le 9 décembre 2009.

Notes de cours sur les modèles booléens (série de cours effectuée à Chambéry):

• Introduction aux modèles booléens (Algèbres de Boole, notion de modèle booléen, notion de modèle plein, quotient par un ultrafiltre, ultra-produits et ultra-puissances, liens avec l'analyse non standard.)
• Modèles booléens de ZFC (Construction de V^(B), mélange et principe du maximum, valeur de vérité dans une sous-algèbre, satisfaction des axiomes de ZFC, ordinaux et cardinaux dans V^(B), construction par forcing, négation de l'hypothèse du continu.)

Le module d'extraction classique pour Coq et l'évaluateur Jivaro qui permet d'exécuter les programmes extraits sont maintenant disponibles.