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/