photo of mhe

Martín Hötzel Escardó

Also known as Martin Escardo.

Reader in Theoretical Computer Science
School of Computer Science, University of Birmingham
Birmingham B15 2TT, UK

Publications, talks, cv, timetable, teaching
Research interests: Topology, topology in higher-type computation, constructive mathematics, dependent type theory, univalent type theory, domain theory, locale theory, real-number computation. My research often stumbles upon category theory, proof theory and game theory. Functional programming is a useful and enjoyable tool for practical manifestations of theoretical ideas.
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 for engineering too. 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, computatation 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, which is related to topology and domain theory. This is particularly the case for Martin-Löf type theory, and even more so for its univalent extensions, such as Book HoTT (homotopy type theory) and Cubical Type Theory. Constructivity is not a binary notion, but a matter of degree. The correct question is not whether a theorem is constructive, but instead how much information its formulation (type) and proof (inhabitant of the type) give. A good foundation has a rich supply of types and ways to build their inhabitants so that the available amount of information can be precisely expressed.

The above is a probably misleading hint of what my mathematical and computational research are about.

The only difference between reality and fiction is that fiction needs to be credible.
Mark Twain

At least in theoretical things, you never set out to discover something new. You stumble on it and you have the luck to recognise what you've found is something very interesting.
Duncan Haldane

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: 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.

Last modified 4 Oct 2016 GMT.