Alexandre Miquel Paris 7 University - PPS Laboratory Chevaleret site - Office 6C16 Phone: +33 (0)1 44 27 86 91 Fax: +33 (0)1 44 27 86 54 E-mail: My_first_name . My_name @ pps.jussieu.fr

I am maître de conférences (lecturer/assistant professor) in Computer Science at Paris 7 University (Denis Diderot). I do my teaching on the campus of Jussieu, but most of the time I am sitting in my office or walking around in the corridors of the 6th floor of the site of Chevaleret.

My research activity in the laboratory Proofs, Programs and Systems lies on the frontier between theoretical computer science and logic, and deals with the connections between mathematical proofs and (functional) programs through the so-called Curry-Howard correspondence. In this research area, my main interests are:

• Logic (classical, intuitionistic, linear logic) and proof theory (normalisation, cut elimination).
• Type systems in general, and especially their english (polymorphism à la ML), french (polymorphism à la system F, Calculus of Constructions), italian (Curry-style type systems, intersection types) and swedish (dependent types, Martin-Löf type theory) variants.
• Semantics (mainly denotational semantics) of proofs and programs, and especially the semantics of subtyping in coherence spaces.
• Realisability, especially in (intuitionistic and classical) set theory.
• Computer assisted proofs.

Finally, I am an enthousiastic user of Objective Caml and of the proof assistant Coq (developped in the LogiCal project, where I did my first scientific steps).

Some piece of software I wrote can be accessed here.