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. 590-607.
M.H. Escardo
and T. Streicher. The intrinsic topology of Martin-Lof universes. Version of Feb 2016. In Annals of Pure and Applied Logic (subsumes a
draft paper included below with a similar title).
M.H. Escardo and Chuangjie Xu. A constructive manifestation of the Kleene-Kreisel continuous functionals. Accepted for publication in Annals of Pure and Applied Logic, editors Thierry Coquand, Maria Emilia Maietti, Giovanni Sambin and Peter Schuster.
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 119-141.
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.
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.
The old version is kept here as it is linked externally, and it won't be modified. The new version is better adapted to univalent type theory, but more work will be done in this direction.
Last
updated 14th September 2017.
M.H. Escardo. The
intrinsic topology of a Martin-Lof 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 764-784. An abstract for this paper was presented at Types'2011.
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).
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).
M.H. Escardo and Paulo Oliva. Searchable Sets, Dubuc-Penon Compactness, Omniscience Principles, and the Drinker Paradox. In CiE 2010 (Computability in Europe) booklet.
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).
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".
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.
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.
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.
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).
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
M.H. Escardo. Function-space
compactifications of function spaces.
Topology and its Applications,
volume 120, issue 3, pp. 441-463, May 2002.
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.
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.
M.H. Escardo and
T. StreicherInduction 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.
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.
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.
ECS-LFCS-97-374 (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 376-386.
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.
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.
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.
M.H. Escardo. Computing with real numbers represented as infinite sequences of digits in Haskell.
CCA'2009 tutorial, August 2009, based on older stuff.
M.H. Escardo. Notes on
compactness. 8th April 2005, updated 12th Sept 2005. (Expanded
version of a previous note called Synthetic compactness
revisited.)
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).
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.
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.
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.