### Martín Escardó

School of Computer Science

University of Birmingham

UK

## Topology for functional programming

#### Abstract

The central notion of topology is that of continuity of functions, closely followed in importance by that of compactness of sets. In computation with infinite objects, continuity amounts to the fact the finite parts of the output can depend only on finite parts of the input. This idea occurs in Brouwerian intuitionistic mathematics, and in Scott-style denotational semantics, and more recently also in operational semantics of programming languages. In this course I will explain continuity and compactness from a computational point of view, and show how they can be used to construct seemingly impossible functional programs that explore an infinite search space in a finite amount of time. I will also illustrate this with various applications.

#### Course materials

- M. Escardó. Topology for functional programming. Slides
for EWSCS '12, 2012. [pdf]

Haskell code [hs]

Agda code [rendered as html], [zip of agda files] - M. Escardó. Synthetic topology of data types and classical
spaces. In J. Desharnais, P. Panangaden, eds.,
*Proc. of Wksh. on Domain-theoretic Methods for Probabilistic Processes (Holetown, Barbados, Apr. 2003)*, v. 87 of*Electron. Notes in Theor. Comput. Sci.*, pp. 21-156. Elsevier, 2004. [doi: 10.1016/j.entcs.2004.09.017] - M. Escardó and W. K. Ho. Operational domain theory and topology
of sequential programming languages.
*Inform. and Comput.*, v. 207, n. 3, pp. 411-437, 2009. [doi: 10.1016/j.ic.2008.12.003] - M. Escardó. Exhaustible sets in higher-type
computation.
*Logical Methods in Computer Science*, v. 4, n. 3, article 3, 2008. [doi: 10.2168/lmcs-4(3:3)2008] - M. Escardó, P. Oliva. What sequential games, the Tychonoff
theorem and the double-negation shift have in common. In
*Proc. of 2010 ACM SIGPLAN Wksh. on Mathematically Structured Functional Programming, MSFP 2010 (Baltimore, MD, Sept. 2010)*, pp. 21-32. ACM Press, 2010. [doi: 10.1145/1863597.1863605]

Last changed **
March 3, 2012 22:16 EET**
by
local organizers, ewscs12(at)cs.ioc.ee

EWSCS'12 page:
//cs.ioc.ee/ewscs/2012/