Martín Escardó's published and unpublished work available online
(Research notes and mathematical and computational Haskell and Agda developments are also available below.)
 M.H. Escardo.
The CantorSchröderBernstein Theorem for ∞groupoids, arXiv:2002.07079, 13th February 2020. There is also blog post at the Homotopy Type Theory website, and an Agda version of the proof.
 M.H. Escardo.
Compact, totally separated and wellordered types in univalent mathematics. Presented at Types 2019. Agda development.

 M.H. Escardo.
Introduction to Univalent Foundations of Mathematics with Agda, March 2019. This is an html document. There is also a pdf version automatically generated from the html version.

 M.H. Escardo.
Injective types in univalent mathematics, March 2019.

 M.H. Escardo.
Agda development of various new theorems in
univalent mathematics. 20102020∞, under continuous development. Many results haven't been published other than in this Agda development, which is also available at github.
 M.H. Escardo.
A selfcontained, brief and complete formulation of Voevodsky's Univalence Axiom, March 2018, arXiv:1803.02294. Includes Agda code as an ancillary file.

 M.H. Escardo.
Agda in a Hurry. Concise tutorial (written for Haskell programmers) to get started with Agda, 5th October 2017.

 M.H. Escardo and Cory Knapp. Partial elements and recursion via dominances in univalent type theory. CSL'2017.
pdf.

 Auke Booij, M.H. Escardo, Peter L. Lumsdaine and Mike Shulman. Parametricity, automorphisms of the universe, and excluded middle. Accepted for publication.
arXiv:1701.05617.

 M.H. Escardo and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the CurryHoward interpretation. TLCA'2015.
pdf ,
Agda version,
slides for the IHP 2014 talk,
slides for the MittagLeffler 2015 talk.
slides for the TLCA'2015 talk.

 Nicolai Kraus, M.H. Escardo, T. Coquand, T. Altenkirch. Notions of anonymous existence in MartinLoef Type Theory. In LMCS.
pdf, Agda formalization (also as a zip file).

 M.H. Escardo and Paulo Oliva. The Herbrand Functional Interpretation of the Double Negation Shift. Journal of Symbolic Logic, Volume 82, Issue 2, June 2017, pp. 590607.
pdf.

 M.H. Escardo and A. Simpson. Abstract Datatypes for Real Numbers in Type Theory. RTA/TLCA'2014.
pdf.

 M.H. Escardo
and T. Streicher. The intrinsic topology of MartinLof universes. Version of Feb 2016. In Annals of Pure and Applied Logic (subsumes a
draft paper included below with a similar title).
pdf.

 M.H. Escardo and Chuangjie Xu. A constructive manifestation of the KleeneKreisel continuous functionals. Accepted for publication in Annals of Pure and Applied Logic, editors Thierry Coquand, Maria Emilia Maietti, Giovanni Sambin and Peter Schuster.
pdf , Agda browsable in html,
zip file

 T. Coquand, N.A. Danielsson, M.H. Escardo, U. Norell and Chuangjie Xu. Negative consistent axioms can be postulated without loss of canonicity. 3page note.
pdf.

 M.H. Escardo. Continuity of Godel's system T functionals via effectful forcing. MFPS'2013. Electronic Notes in Theoretical Computer Science 01/2013, volume 298, pages 119141.
pdf,
Agda (with combinatory version of system T),
Agda without comments,
Agda using Church encoding of dialogues,
Agda internalizing the modulus of continuity,
Agda (with lambdacalculus version of system T),
more.

 Chuangjie Xu and M.H. Escardo. A constructive model of uniform continuity, M. Hasegawa (Ed.): TLCA 2013, LNCS 7941, pp. 236249. Springer, Heidelberg 2013.
pdf, Agda

 Nicolai Kraus, M.H. Escardo, T. Coquand, T. Altenkirch. Generalizations of Hedberg's Theorem, M. Hasegawa (Ed.): TLCA 2013, LNCS 7941, pp. 173188. Springer, Heidelberg 2013.
pdf, Agda,
A family of types that fail to be provably collapsible (also in Agda),
Constant choice.

 M.H. Escardo. Constructive decidability of
classical continuity. Mathematical Structures in Computer Science, published online 23 December 2014.
pdf

 M.H. Escardo. The
intrinsic topology of a MartinLof universe, March 2012.
 M.H. Escardo. Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics. The Journal of Symbolic Logic (JSL),
Volume 78, Number 3, September 2013, pages 764784. An abstract for this paper was presented at Types'2011.
 M.H. Escardo, Paulo Oliva, and Thomas Powell. System T and the product of selection functions. CSL'2011.
pdf
 M.H. Escardo and Paulo Oliva. Bar recursion and products of selection functions. Journal of Symbolic Logic, 80(1):128, 2015.
pdf
 M.H. Escardo and Paulo Oliva. Sequential Games and Optimal Strategies.
In Proceedings of the Royal Society A (it is among the top 10 downloaded papers for 2011), December 2010.
pdf

 M.H. Escardo and Paulo Oliva. The Peirce translation. To appear in APAL (revised version of a paper that was previously available here). A condensed version was published in conference proceedings (see below).
pdf

 M.H. Escardo and Paulo Oliva. What Sequential Games, the Tychonoff Theorem and the
DoubleNegation Shift have in Common. In MSFP 2010 (ACM SIGPLAN
Mathematically Structured Functional Programming, ACM Press).
pdf,
companion Haskell and Agda files.

 M.H. Escardo and Paulo Oliva. The Peirce translation and the double negation shift. CiE 2010 (Computability in Europe, LNCS).
pdf

 M.H. Escardo and Paulo Oliva. Computational interpretations of analysis via products of selection functions. CiE 2010 (Computability in Europe, LNCS).
pdf

 M.H. Escardo and Paulo Oliva. Searchable Sets, DubucPenon Compactness, Omniscience Principles, and the Drinker Paradox. In CiE 2010 (Computability in Europe) booklet.
pdf
See also the companion programs/proofs in Agda.
 M.H. Escardo and Paulo Oliva. Selection functions, bar recursion, and backward induction. In Mathematical Structures in Computer Science, Volume 20, Issue 2, April 2010, Cambridge University Press.
pdf

 M.H. Escardo. Algorithmic solution of highertype equations. To appear in JLC. A condensed version was published in CiE'2009 conference proceedings (see below).
pdf

 M.H. Escardo. Intersections of compactly many open sets are open. arXiv:2001.06050. (A previous version of this paper (almost identical) has been available since 2005 under the name "notes on compactness".)
pdf

 M.H. Escardo. Computability of continuous solutions of highertype equations. Lecture Notes in Computer Science 5635 (Mathematical Theory and Computational Practice), Proceedings of the 5th Conference on Computability in Europe, CiE 2009, Springer.
pdf

 M.H. Escardo. Semidecidability of may, must and probabilistic testing in a highertype setting.
Electronic Notes in Theoretical Computer Science,
Volume 249, 8 August 2009, Pages 219242,
Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics (MFPS 2009), Elsevier.
pdf

 M.H. Escardo. Exhaustible sets in highertype computation.
In Logical Methods in Computer Science, volume 4, issue 3, paper 4, 2008, selected papers of the conference Logic in Computer Science 2007, editors Erich Graedel, Luke Ong, Andrew M. Pitts.
pdf
 M.H. Escardo. Infinite sets that admit fast exhaustive
search. In LICS'2007, IEEE, pages 443452, Poland, Wroclaw, July.
pdf (paper),
hs (companion Haskell program extracted from the paper).

 M.H. Escardo and W.K. Ho. Operational domain theory
and topology of sequential programming languages. 18 November
2006, revised May 2008. Subsumes LICS publication below with approximately the same title. Information and Computation 207 (2009) 411–437.
pdf.

 J. Raymundo MarcialRomero and M.H. Escardo. Semantics of a sequential language for exact realnumber computation. Subsumes LICS publication below with the same title. Theoretical Computer Science, 379 (2007), no. 12, 120141.
pdf, ps, dvi.

 F. De Jaeger, M.H. Escardo and G. Santini. On the
computational content of the Lawson topology, Theoretical
Computer Science 357 (2006) 230240, Elsevier.
pdf, ps, ps.gz, dvi, dvi.gz.

 M.H. Escardo. Compactly generated Hausdorff locales.
Annals of Pure and Applied Logic, Elsevier, volume 137, issues 13, pages 147163, 2006.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.
 M.H. Escardo and W.K. Ho. Operational domain theory
and topology of a sequential programming language. 31st December
2004, slightly revised 19th July 2005. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, June 2005, pages 427436.
pdf, ps, ps.gz, dvi, dvi.gz.

 M.H. Escardo, M. Hofmann and T. Streicher. On the nonsequential nature of the intervaldomain model of exact realnumber computation. Mathematical Structures in Computer Science,
Cambridge University Press, volume 14, number 6, pages 803814, December 2004.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 M.H. Escardo. Synthetic topology of data types and
classical spaces. ENTCS, Elsevier, volume 87, pages 21156, November
2004.
pdf, ps, ps.gz,
dvi, dvi.gz
.

 M.H. Escardo,
J.D. Lawson and
A. Simpson.
Comparing cartesian closed categories of (core) compactly generated spaces.
Topology and its Applications, Elsevier, volume 143,
issues 13, pages 105145, August 2004.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 J.R. MarcialRomero and M.H. Escardo. Semantics of a sequential language for exact realnumber computation.
Proceedings of the 19th Annual IEEE Symposium on
Logic in Computer Science, pp. 426435, Jul 2004.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 M.H. Escardo. Joins in the frame of nuclei.
Applied Categorical Structures,
Springer (formerly Kluwer), volume 11, number 2, pp. 117124, April 2003.
pdf, ps, ps.gz, dvi,
dvi.gz.

 M.H. Escardo. Injective locales over perfect embeddings and algebras of the upper powerlocale monad.
Applied General Topology, volume 4, number 1, pp. 193200, 2003.
pdf, ps, ps.gz, dvi, dvi.gz.

 M.H. Escardo and
T. Streicher.
In domain realizability, not all functionals on C[1,1] are continuous,
Mathematical Logic Quarterly, Wiley, volume 48, suppl. 1, pages 4144,
October 2002.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 A. Bauer,
M.H. Escardo and
A. Simpson.
Comparing functional paradigms for exact realnumber
computation (extended abstract).
Proceedings ICALP 2002, Springer, LNCS 2380, pp. 488500, 2002.
pdf, ps.
Unpublished full version (needs rewriting): pdf, ps.

 M.H. Escardo. Functionspace
compactifications of function spaces.
Topology and its Applications,
volume 120, issue 3, pp. 441463, May 2002.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.
 M.H. Escardo and
R. Heckmann. Topologies on spaces of continuous functions.
Topology Proceedings, volume 26,
number 2, pp. 545564, 20012002.
pdf, ps, ps.gz, dvi,
dvi.gz.
 M.H. Escardo and
A. Simpson.
A universal characterization of the closed Euclidean interval
(extended abstract).
Proceedings of the
16th Annual IEEE Symposium on Logic in Computer Science, pp.115125.
Boston, Massachusetts, June 1619, 2001.
paper,
slides presented at MAP'2011 in Leiden, draft full version (a more polished full version will be eventually available, for the moment the paper is more readable).

 M.H. Escardo.
The regularlocallycompact coreflection of a stably locally compact locale.
Journal of Pure and Applied Algebra,
Elsevier, volume 157, number 1, pages 4155, March 2001.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 A.
E. and M.H. Escardo. Integration in Real PCF.
Information and Computation, Elsevier (Academic Press),
volume 160, numbers 12, 128166, July 2000.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 M.H. Escardo and R. Flagg.
Semantic domains, injective spaces and monads.
ENTCS, Elsevier, volume 20, April 1999.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.
 M.H. Escardo.
On the compactregular coreflection of a stably compact locale.
ENTCS, Elsevier, volume 20, April 1999.
pdf, ps, ps.gz, dvi, dvi.gz.
 M.H. Escardo and
T. Streicher
Induction and recursion on the partial real line with applications to Real PCF. Theoretical Computer Science, Elsevier, volume 210, number 1, pages 121157, January 1999.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.
 M.H. Escardo. Properly injective spaces and function spaces.
Topology and its
Applications, Elsevier, volume 89, number 12, pp. 75120, 1998.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 T. Erker, M.H. Escardo and
K. Keimel.
The waybelow relation of function spaces over semantic domains.
Topology and its Applications, Elsevier, volume 89, number 12, pp. 6174, 1998.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.
 M.H. Escardo. Effective and sequential definition by cases on the reals via infinite signeddigit numerals. ENTCS, Elsevier, vol 13, 1998.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.
 D. Pavlovic
and M.H. Escardo. Calculus in coinductive form.
Proceedings of the 13th Annual IEEE Symposium on
Logic in Computer Science. Indiana, USA, June 1998.
Electronically available as Technical Report 97:05,
School of Cognitive and Computing
Sciences,
University of Sussex.

 M.H. Escardo. Injective spaces via the filter monad.
Topology Proceedings, volume 22, pp. 97110, 1997.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 M.H. Escardo.
PCF extended with real numbers: a domaintheoretic approach to
higherorder exact real number computation.
PhD thesis under the supervision of M.B. Smyth at the
Department of Computing of
Imperial
College, University of
London, submitted in November 1996 and defended in February 1997.
Published as
Technical Report
number
ECSLFCS97374 of the LFCS, Division of Informatics , University of
Edinburgh, November 1997.
ECSLFCS97374 (follow this link and then find file at the bottom).
 M.H. Escardo and
T. Streicher.
Induction and recursion on the partial real line via
biquotients of bifree algebras.
Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science.
Warsaw, Poland, June 1997, pages 376386.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.
 P. Potts and
A. E. and M.H. Escardo. Semantics of exact real arithmetic.
Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science.
Warsaw, Poland, June 1997, pages 248257.
ps,
ps.gz.
 A.
E. and M.H. Escardo. Integration in Real PCF (extended abstract). Proceedings of the 11th Annual IEEE Symposium on Logic In Computer Science,
New Brunswick, New Jersey, USA, June 1996, pages 382393.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.
 M.H. Escardo.
Real PCF extended with ∃ is universal.
Eds. A.E., A., Jourdan, S., McCusker, G., Proceedings of the 3rd
Workshop on Theory and Formal Methods, IC Press, pages 1324, April 1996.
Christ Church, Oxford, 1996.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

PCF extended with real numbers.
Theoretical Computer Science,
Elsevier, volume 162, issue 1, pp. 79115, August 1996.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

Research and teaching notes
 M.H. Escardo. Dummett disjunction in MartinLöf Type Theory.
31 March 2016, Unpublished research note.
html.

 Chuangjie Xu and M.H. Escardo. Universes in sheaf models.
February 2016, Unpublished research note.
pdf.

 M.H. Escardo. Using Yoneda rather than MartinLof's induction principle J to present the identity type in MLTT. Unpublished note. 7 May 2015.
html ,
Agda.

 T. Coquand and M.H. Escardo. The geometry of constancy. Unpublished note, to be presented at HoTT/UF. May 2015.
pdf abstract,
talk at HoTT/UF in Warsaw 2015,
cubicaltt code with full formal proofs.

 M.H. Escardo. Computing with real numbers represented as infinite sequences of digits in Haskell.
CCA'2009 tutorial, August 2009, based on older stuff.
zip file with Haskell programs and scripts.
There is also a literate program derived from this used for a talk in Fun in the Afternoon (March 2011).

 M.H. Escardo. Kreisel's counterexample to full
abstraction of the settheoretical model of Goedel's system T.
23rd July 2007.
pdf.

 M.H. Escardo. Notes on
compactness. 8th April 2005, updated 12th Sept 2005. (Expanded
version of a previous note called Synthetic compactness
revisited.)
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 M.H. Escardo. [Synthetic] Topology via higherorder intuitionistic logic, version of 18 March 2004, made available here 07 Oct 2010, presented at MFPS in Pittsburgh in 2004. These are first steps, which I intended to eventually carry out, but I was occupied with many other things. Because Davorin Lesnik has produced a very nice PhD thesis taking this as a starting point, under the advice of Andrej Bauer, I decided to make my unfinished paper publicly available (it may contain mistakes, particularly in the claims left without proofs).
pdf.


 M.H. Escardo. Mathematical foundations of functional programming with real numbers.
Notes for a course delivered at the Midlands Graduate School in the
Foundations of Computer Science, Leicester, Mar 31, Apr 1, 2003.
pdf.

 M.H. Escardo. Introduction to Real PCF.
Notes for an invited talk at the 3rd Real Numbers and Computers
Conference (RNC3), l'Université Pierre et Marrie Curie,
Paris, April 1998.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.
 M.H. Escardo. Introduction to exact
numerical computation.
Notes for a tutorial course at the International
Symposium on Symbolic and Algebraic Computation (ISSAC), St
Andrews, 69 August 2000.
pdf,
html,
ps,
ps.gz,
dvi,
dvi.gz.
 M.H. Escardo. The patch frame of the Lawson dual of a stably continuous frame. 23 May 2000.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 M.H. Escardo. Spatiality of the patch frame. 18 May 2000.
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 M.H. Escardo. The interpolation property of the waybelow relation of
a continuous poset. 18 Mar 2000. It has been included in the paper
Functionspace compactifications of function spaces and in the book "Continuous lattices and domains" (CUP 2003) by GHKLMS via Keimel.
pdf, ps, ps.gz, dvi, dvi.gz.


 M.H. Escardo. A metric model of PCF.
Presented at the
Workshop on Realizability Semantics and Applications,
June 30July 1, 1999 (associated to the Federated Logic Conference,
held in Trento, June 29July 12, 1999).
pdf,
ps,
ps.gz,
dvi,
dvi.gz.

 Seemingly impossible functional programs (in Haskell).
 Real number computation in Haskell with real numbers represented as infinite sequences of digits.
 A Haskell monad for infinite search in finite time (in Haskell).
 Running a classical proof with choice in Agda (a blog post summarizes this).
 What Sequential Games, the Tychonoff Theorem and the DoubleNegation Shift have in Common.
 Various new theorems in constructive mathematics developed in a constructive univalent type theory using Agda.
This includes, among other things:
This is also briefly reported as a blog post with links to an older version.
 Using Yoneda rather than J to present MartinLöf's identity type.
 Continuity of Godel's system T functionals via effectful forcing.
 The inconsistency of a Brouwerian continuity principle with the CurryHoward interpretation.
 Univalent logic.
 A small type of propositions a la Voevodsky in Agda. This uses Type:Type in only one module.
 This uses rewriting instead.
 This lives with the fact that the type of propositions is large, and also discusses a large propositional truncation a la Voevodsky and its relation to the small one (if it exists).
 This uses rewriting only to make propositional truncations a la Voevodsky small. Everything else retains its native universe level.
 Agda discussion about propositional truncation, function extensionality, and turning any factorization via the propositional truncation of the domain of a function into a judgmental one. It includes the fact that the interval is the propositional truncation of the booleans, which gives the germ of the idea for the factorization.
 Generalizations of Hedberg's Theorem.
 The empty type has a constant endomap (the identity function). Any type that has a given point has a constant endomap (that maps everything to that point). If every type has a constant endomap, then every type has decidable equality, which implies WLPO and other constructive taboos.
 Dummett disjunction in MartinLöf Type Theory.
This material is presented to ensure timely dissemination of scholarly
and technical work. Copyright and all rights therein are retained by
authors or by other copyright holders, usually the publishers. All
persons and robots copying this information are expected to adhere to
the terms and constraints invoked by each author's copyright. In most
cases, these works may not be reposted without the explicit permission
of the copyright holder.
Martin Escardo
m.escardo@cs.bham.ac.uk
Last modified: Friday February 21 10:6:7 UTC 2020