Publications, talks, cv,
timetable,
teachingResearch interests: Topology in higher-type computation, constructive mathematics, dependent type theory, univalent type theory, domain theory, locale theory, game theory.
The only difference between reality and fiction is that fiction needs to
be credible. Mark Twain.

In mathematics and the theory of computation, what is interesting
is what is incredible but true, defying our intuitions, giving new
light to our understanding. This is of course the case for all
sciences, and even (more?) for engineering, with "true"
replaced by "doable".

In the theory of higher-type computation, in the sense of Kleene and
Kreisel, my favourite example is the characterization of the sets that
can be exhaustively searched by an algorithm, in the sense of Turing,
in finite time, as those which are topologically compact.

In
particular, this understanding gives examples of infinite sets that
can be completely inspected in finite time in an algorithmic way, which perhaps defies intuition.

I am also interested in constructive mathematics, which I see as a
generalization, rather than as a restriction, of classical
mathematics. In constructive mathematics, in the way I conceive it,
computability is a side-effect, rather than its foundation.

What
distinguishes classical and constructive mathematics is that the
latter is better equipped to explicitly indicate the amount of
information given by its definitions, theorems and proofs. This is
particularly the case for Martin-Loef type theory, and even more for
its univalent extensions.

The above is a (probably misleading) hint of what my research is about.

I joined Birmingham University
in September 2000. My first degree was from the Universidade
Federal do Rio Grande Sul,
where I also obtained an MSc degree by research. During my undergraduate
and MSc studies, I worked in industry.
I then went to
Imperial College
of the University of London in October 1993 for my PhD under the supervision of Mike B. Smyth. After completing this in April 1997, I was a
postdoc for one year at Imperial, a lecturer at the University
of Edinburgh for two years, and then at the University
of St Andrews for one year, after which I came here and have happily been part of a vibrant theory research group.
email: m.escardo@cs.bham.ac.uk
office: 212 phone: +44 121 414 2797 fax: +44 121 414
4281

directions: Look for building Y9 in the yellow zone of
the Edgbaston
campus map. This is
about 1 minute walking time from the train station. Turn left when you
exit the station, and walk for about 30 meters. Our building is the
right-hand one of two red-brick twin buildings facing each other.