Dr Martin Escardo Bsc MSc PhD

Dr Martin Escardo

School of Computer Science
Reader in Theoretical Computer Science

Contact details

Email
m.escardo@cs.bham.ac.uk
View my research portal
Address
School of Computer Science
University of Birmingham
Edgbaston
Birmingham
B15 2TT
UK

Martin Escardo joined University of Birmingham in September 2000. His first degree was from the Universidade Federal Do Rio Grande Sul where he also obtained an MSc degree by research. During his undergraduate and MSc studies, he worked in industry. He then went to Imperial College of the University of London in October 1993 for his PhD under the supervision of Mike.B.Smyth. After completing this in April 1997, he was a postdoc for one year at Imperial, a lecturer at the University of Edingburgh for two years, and then at the University of St Andrews for one year before joining the University of Birmingham.

For more information, please see Martin's Computer Science profile.

Qualifications

  • BSc Computer Science – UFRGS
  • MSc by research, Computer Science - UFRGS
  • PhD in Theoretical Computer Science – Imperial College

Research

  • Homotopy type theory

  • Univalent mathematics

  • Martin-Loef type theory

  • Constructive mathematics

  • Domain theory

  • Topology in the theory of computation

Publications

Recent publications

Article

Kraus, N, Escardo, M, Coquand, T & Altenkirch, T 2017, 'Notions of Anonymous Existence in Martin-Löf Type Theory', Logical Methods in Computer Science, vol. 13, no. 1, pp. 1-36. https://doi.org/10.23638/LMCS-13(1:15)2017

Escardó, M & Xu, C 2016, 'A constructive manifestation of the Kleene–Kreisel continuous functionals', Annals of Pure and Applied Logic, vol. 167, no. 9, pp. 770-793. https://doi.org/10.1016/j.apal.2016.04.011

Escardó, MH & Streicher, T 2016, 'The intrinsic topology of Martin-Löf universes', Annals of Pure and Applied Logic, vol. 167, no. 9, pp. 794-805. https://doi.org/10.1016/j.apal.2016.04.010

Escardó, M 2015, 'Constructive decidability of classical continuity', Mathematical Structures in Computer Science, vol. 25, no. Special Issue 7, pp. 1578-1589. https://doi.org/10.1017/S096012951300042X

Escardó, M & Oliva, P 2015, 'Bar recursion and products of selection functions', Journal of Symbolic Logic, vol. 80, no. 01, pp. 1-28. https://doi.org/10.1017/jsl.2014.82

Escardo, M & Oliva, P 2012, 'The Peirce translation', Annals of Pure and Applied Logic, vol. 163, no. 6, pp. 681-692. https://doi.org/10.1016/j.apal.2011.11.002

Escardo, M & Oliva, P 2011, 'Sequential Games and Optimal Strategies', Royal Society of London. Proceedings A. Mathematical, Physical and Engineering Sciences, vol. 467, no. 2130, pp. 1519-1545. https://doi.org/10.1098/rspa.2010.0471

Escardo, M & Oliva, P 2010, 'Selection Functions, Bar Recursion and Backward Induction', Mathematical Structures in Computer Science, vol. 20, no. 2, pp. 127-168. https://doi.org/10.1017/S0960129509990351

Conference contribution

Escardo, M & Knapp, C 2017, Partial Elements and Recursion via Dominances in Univalent Type Theory. in V Goranko & M Dam (eds), Proceedings of 26th EACSL Annual Conference on Computer Science Logic (CSL2017)., 21, Leibniz International Proceedings in Informatics (LIPIcs), vol. 82, Schloss Dagstuhl, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Stockholm, Sweden, 20/08/17. https://doi.org/10.4230/LIPIcs.CSL.2017.21

Booij, A, Escardo, M, Lumsdaine, PL & Shulman, M 2017, Parametricity, automorphisms of the universe, and excluded middle. in Proceedings of 22nd International Conference on Types for Proofs and Programs, TYPES 2016. Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl, 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, 23/05/16.

Escardo, M & Xu, C 2015, The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. in T Altenkirch (ed.), 13th International Conference on Typed Lambda Calculi and Applications, Proceedings. LIPICS - Leibniz International Proceedings in Informatics, vol. 38, Schloss Dagstuhl, pp. 153-164, 13th International Conference on Typed Lambda Calculi and Applications, Warsaw, Poland, 1/07/15. https://doi.org/10.4230/LIPIcs.TLCA.2015.153

Escardó, MH & Simpson, A 2014, Abstract datatypes for real numbers in type theory. in G Dowek (ed.), Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. vol. 8560 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8560 LNCS, Springer, pp. 208-223, 25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 14/07/14. https://doi.org/10.1007/978-3-319-08918-8-15

Escardo, M & Oliva, P 2010, Computational Interpretations of Analysis via Products of Selection Functions. in F Ferreira, B Lowe, E Mayordomo & LM Gomes (eds), Programs, Proofs, Processes: 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30 – July 4, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6158, Springer, pp. 141-150. https://doi.org/10.1007/978-3-642-13962-8_16

Paper

Escardo, M, Oliva, P, Powell, T & Bezem, M 2011, 'System T and the Product of Selection Functions' Paper presented at Computer Science Logic (CSL'11) - Proceedings of the 25th International Workshop/20th Annual Conference of the EACSL, 31/08/11, pp. 233-247.

Escardo, M & Oliva, P 2010, 'What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common' Paper presented at Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming - MSFP '10, New York, New York, USA, 25/09/10, pp. 21-32. https://doi.org/10.1145/1863597.1863605

View all publications in research portal