Alexandre Miquel
I am professor in the
IMERL,
Facultad de Ingeniería,
Universidad de la República
(Montevideo).
I coordinate the activities of the
Logic Team / Equipo de Lógica.
Formerly, I was maître de conférences in the
LIP at
ENS de Lyon.
And even before, I was working in the
PPS lab
at the University Paris
Diderot (Paris 7).
Research
My research activity lies at the frontier between theoretical computer
science and mathematical logic, and deals with the connections between
mathematical proofs and computer programs, through the
so-called Curry-Howard correspondence.
In this framework, my main scientific interests are:
- Classical realizability and its connections with Cohen
forcing.
- Logic (classical/intuitionistic/linear)
and proof theory.
- Type systems (ML languages, System F, Type Theory,
Pure Type Systems, etc.)
- Semantics of proofs and programs
Here are my publications.
Courses and seminars
Talks/Charlas
Diapositivas de mi charla:
Introducción al Análisis no estándar.
Some slides about intuitionistic and classical realizability:
Teaching
In July 2014, I gave a Tutorial about classical realizability and forcing
at the Logic Colloquium in Vienna:
In the first semester of 2014, I gave a postgraduate course of
advanced set theory:
An Introduction to Forcing.
In April 2014, I gave a series of lectures about the computational
interpretation of proofs and realizability for the PhD school at the
CIRM in Luminy. Here are the slides:
UdelaR -
Fing -
IMERL -
Publications