Martín Escardó's research papers available on line

(Research notes are also available below.)

  1. M.H. Escardo. Continuity of Godel's system T functionals via effectful forcing. Accepted for MFPS'2013.

    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 lambda-calculus version of system T), more.

  2. Chuangjie Xu and M.H. Escardo. A constructive model of uniform continuity, M. Hasegawa (Ed.): TLCA 2013, LNCS 7941, pp. 236-249. Springer, Heidelberg 2013.

    pdf, Agda

  3. Nicolai Kraus, M.H. Escardo, T. Coquand, T. Altenkirch. Generalizations of Hedberg's Theorem, M. Hasegawa (Ed.): TLCA 2013, LNCS 7941, pp. 173-188. Springer, Heidelberg 2013.

    pdf, Agda, A family of types that fail to be provably collapsible (also in Agda), Constant choice.

  4. M.H. Escardo. Constructive decidability of classical continuity. To appear in MSCS.

    pdf

  5. M.H. Escardo. Formalization in Agda of various new theorems in constructive mathematics. There is also a zip file with all the Agda files. Last updated 5th March 2013 21:20 GMT.

  6. M.H. Escardo. The intrinsic topology of a Martin-Lof universe, March 2012.

  7. M.H. Escardo. Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics. To appear in The Journal of Symbolic Logic (JSL), Volume 78, Number 3, September 2013. An abstract for this paper was presented at Types'2011.

  8. M.H. Escardo, Paulo Oliva, and Thomas Powell. System T and the product of selection functions. CSL'2011.

    pdf

  9. M.H. Escardo and Paulo Oliva. Bar recursion and products of selection functions. Submitted for publication to a journal.

    pdf

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

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

  12. M.H. Escardo and Paulo Oliva. What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common. In MSFP 2010 (ACM SIGPLAN Mathematically Structured Functional Programming, ACM Press).

    pdf, companion Haskell and Agda files.

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

    pdf

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

    pdf

  15. M.H. Escardo and Paulo Oliva. Searchable Sets, Dubuc-Penon Compactness, Omniscience Principles, and the Drinker Paradox. In CiE 2010 (Computability in Europe) booklet.

    pdf

    See also the companion programs/proofs in Agda.

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

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

    pdf

  18. M.H. Escardo. Intersections of compactly many open sets are open. Submitted for publication June 2009. A previous version of this paper (almost identical) has been available since 2005 under the name "notes on compactness".

    pdf

  19. M.H. Escardo. Computability of continuous solutions of higher-type 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

  20. M.H. Escardo. Semi-decidability of may, must and probabilistic testing in a higher-type setting. Electronic Notes in Theoretical Computer Science, Volume 249, 8 August 2009, Pages 219-242, Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics (MFPS 2009), Elsevier.

    pdf

  21. M.H. Escardo. Exhaustible sets in higher-type 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

  22. M.H. Escardo. Infinite sets that admit fast exhaustive search. In LICS'2007, IEEE, pages 443-452, Poland, Wroclaw, July.

    pdf (paper), hs (companion Haskell program extracted from the paper).

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

  24. J. Raymundo Marcial--Romero and M.H. Escardo. Semantics of a sequential language for exact real-number computation. Subsumes LICS publication below with the same title. Theoretical Computer Science, 379 (2007), no. 1-2, 120--141.

    pdf, ps, dvi.

  25. F. De Jaeger, M.H. Escardo and G. Santini. On the computational content of the Lawson topology, Theoretical Computer Science 357 (2006) 230--240, Elsevier.

    pdf, ps, ps.gz, dvi, dvi.gz.

  26. M.H. Escardo. Compactly generated Hausdorff locales. Annals of Pure and Applied Logic, Elsevier, volume 137, issues 1-3, pages 147-163, 2006.

    27. pdf, ps, ps.gz, dvi, dvi.gz.

  27. 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 427-436.

    pdf, ps, ps.gz, dvi, dvi.gz.

  28. M.H. Escardo, M. Hofmann and T. Streicher. On the non-sequential nature of the interval-domain model of exact real-number computation. Mathematical Structures in Computer Science, Cambridge University Press, volume 14, number 6, pages 803-814, December 2004.

    pdf, ps, ps.gz, dvi, dvi.gz.

  29. M.H. Escardo. Synthetic topology of data types and classical spaces. ENTCS, Elsevier, volume 87, pages 21-156, November 2004.

    pdf, ps, ps.gz, dvi, dvi.gz .

  30. 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 1-3, pages 105--145, August 2004.

    pdf, ps, ps.gz, dvi, dvi.gz.

  31. J.R. Marcial-Romero and M.H. Escardo. Semantics of a sequential language for exact real-number computation. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 426-435, Jul 2004.

    pdf, ps, ps.gz, dvi, dvi.gz.

  32. M.H. Escardo. Joins in the frame of nuclei. Applied Categorical Structures, Springer (formerly Kluwer), volume 11, number 2, pp. 117-124, April 2003.

    pdf, ps, ps.gz, dvi, dvi.gz.

  33. M.H. Escardo. Injective locales over perfect embeddings and algebras of the upper powerlocale monad. Applied General Topology, volume 4, number 1, pp. 193-200, 2003.

    pdf, ps, ps.gz, dvi, dvi.gz.

  34. 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 41-44, October 2002.

    pdf, ps, ps.gz, dvi, dvi.gz.

  35. A. Bauer, M.H. Escardo and A. Simpson. Comparing functional paradigms for exact real-number computation (extended abstract). Proceedings ICALP 2002, Springer, LNCS 2380, pp. 488-500, 2002.

    pdf, ps. Unpublished full version (needs rewriting): pdf, ps.

  36. M.H. Escardo. Function-space compactifications of function spaces. Topology and its Applications, volume 120, issue 3, pp. 441-463, May 2002.

    pdf, ps, ps.gz, dvi, dvi.gz.

  37. M.H. Escardo and R. Heckmann. Topologies on spaces of continuous functions. Topology Proceedings, volume 26, number 2, pp. 545-564, 2001-2002.

    pdf, ps, ps.gz, dvi, dvi.gz.

  38. 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.115--125. Boston, Massachusetts, June 16-19, 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).

  39. M.H. Escardo. The regular-locally-compact coreflection of a stably locally compact locale. Journal of Pure and Applied Algebra, Elsevier, volume 157, number 1, pages 41-55, March 2001.

    pdf, ps, ps.gz, dvi, dvi.gz.

  40. A. E. and M.H. Escardo. Integration in Real PCF. Information and Computation, Elsevier (Academic Press), volume 160, numbers 1-2, 128-166, July 2000.

    pdf, ps, ps.gz, dvi, dvi.gz.

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

  42. M.H. Escardo. On the compact-regular coreflection of a stably compact locale. ENTCS, Elsevier, volume 20, April 1999.

    pdf, ps, ps.gz, dvi, dvi.gz.

  43. 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 121-157, January 1999.

    pdf, ps, ps.gz, dvi, dvi.gz.

  44. M.H. Escardo. Properly injective spaces and function spaces. Topology and its Applications, Elsevier, volume 89, number 1-2, pp. 75-120, 1998.

    pdf, ps, ps.gz, dvi, dvi.gz.

  45. T. Erker, M.H. Escardo and K. Keimel. The way-below relation of function spaces over semantic domains. Topology and its Applications, Elsevier, volume 89, number 1-2, pp. 61-74, 1998.

    pdf, ps, ps.gz, dvi, dvi.gz.

  46. M.H. Escardo. Effective and sequential definition by cases on the reals via infinite signed-digit numerals. ENTCS, Elsevier, vol 13, 1998.

    pdf, ps, ps.gz, dvi, dvi.gz.

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

  48. M.H. Escardo. Injective spaces via the filter monad. Topology Proceedings, volume 22, pp. 97-110, 1997.

    pdf, ps, ps.gz, dvi, dvi.gz.

  49. M.H. Escardo. PCF extended with real numbers: a domain-theoretic approach to higher-order 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 ECS-LFCS-97-374 of the LFCS, Division of Informatics , University of Edinburgh, November 1997.

    ECS-LFCS-97-374 (follow this link and then find file at the bottom).

  50. 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 376-386.

    pdf, ps, ps.gz, dvi, dvi.gz.

  51. 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 248-257.

    ps, ps.gz.

  52. 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 382-393.

    pdf, ps, ps.gz, dvi, dvi.gz.

  53. M.H. Escardo. Real PCF extended with \(\exists\) is universal. Eds. A.E., A., Jourdan, S., McCusker, G., Proceedings of the 3rd Workshop on Theory and Formal Methods, IC Press, pages 13-24, April 1996. Christ Church, Oxford, 1996.

    pdf, ps, ps.gz, dvi, dvi.gz.

  54. PCF extended with real numbers. Theoretical Computer Science, Elsevier, volume 162, issue 1, pp. 79-115, August 1996.

    pdf, ps, ps.gz, dvi, dvi.gz.

Research and teaching notes
  1. 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).

  2. M.H. Escardo. Kreisel's counter-example to full abstraction of the set-theoretical model of Goedel's system T. 23rd July 2007.

    pdf.

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

  4. M.H. Escardo. [Synthetic] Topology via higher-order 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.

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

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

  7. 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, 6-9 August 2000.

    pdf, html, ps, ps.gz, dvi, dvi.gz.

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

  9. M.H. Escardo. Spatiality of the patch frame. 18 May 2000.

    pdf, ps, ps.gz, dvi, dvi.gz.

  10. M.H. Escardo. The interpolation property of the way-below relation of a continuous poset. 18 Mar 2000. It has been included in the paper Function-space 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.

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

    pdf, ps, ps.gz, dvi, dvi.gz.

Research blog posts

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: Tuesday 21 May 23:45 BST 2013