Alexandre Miquel Université Paris 7 - Laboratoire PPS Site de Chevaleret - Bureau 6C16 Tél: +33 (0)1 44 27 86 91 Fax: +33 (0)1 44 27 86 54 E-mail: Mon_prénom . Mon_nom @ pps.jussieu.fr

Je suis maître de conférences en informatique à l'Université Paris 7 - Denis Diderot. J'effectue mes enseignements sur le campus de Jussieu, mais la plupart du temps, on peut me trouver dans mon bureau ou dans les couloirs du 6e étage du site de Chevaleret.

Mon activité de recherche au sein du laboratoire Preuves, Programmes et Systèmes 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.

Enfin, je suis un heureux utilisateur du langage Objective Caml (dont on ne clamera jamais assez haut les louanges) et de l'assistant à la démonstration Coq (développé au sein du projet LogiCal, mon « berceau » scientifique).

Certaines de mes réalisations logicielles sont disponibles ici.