Resources for my EWSCS'2012 course on topology for functional programming.

1. The slides.

   Warning: I used the board quite often, with many (most?) things not in the slides, unfortunately.

2. Haskell code used in the lectures, with information and discussion.

   See also the dependency graphs as explained in the Haskell comments, for uniform modulus of continuity 3, 4, 5, 6, 7, 8.

   There is also alternative Haskell code, with less discussion, but more experiments.

   And a C++ implementation of some of this by one of the course students, Ivan Pouzyrevsky, which includes call-by-need.

3. Agda programs/proofs rendered in html for easy navigation with links.

   There is also a zip file with the the Agda files.

   (What is Agda? I recommend this to get started.)

4. Additional material, not in any particular order:
   • Dag Normann's paper Computing with functionals - computability theory or computer science?
   • His slides 50 years of continuous functionals.
   • Andrej Bauer's Mathematics and Computation blog.
   • My post Seemingly impossible functional programs.
   • Andrej's post Double exponentials.
   • My post A Haskell monad for infinite search in finite time.
   • What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common, by Paulo Oliva and myself

     (and Running a classical proof with choice in Agda).

   • My paper Exhaustible sets in higher-type computation.
   • My paper Infinite sets that admit fast exhaustive search.
   • My paper Synthetic topology of data types and classical spaces.
   • Operational domain theory and topology of sequential programming languages, by my former PhD student Ho Weng Kin and myself.
   • Lot's of papers that Paulo Oliva and I wrote with connections of the above and proof theory and program extraction from classical proofs.

   • Dana Scott's seminal paper A type-theoretic alternative to ISWIM, CUCH and OWHY, written in 1969, widely circulated, and then published in 1993.
   • Gordon Plotkin's Pisa notes on domain theory.
   • His seminal paper LCF considered as a programming language.
   • Abramsky and Jung's Domain Theory chapter.
   • Steve Vicker's book Topology via Logic.
   • Mike Smyth's (my PhD supervisor back in the last millenium, 1993-1996, at Imperial College, London) Chapter on Topology, highly recommended.
   • Alex Simpson and Matthias Schroeder's work on Topological domain theory.
   • John Longley's paper Notions of computability at higher types I.
   • His paper On the ubiquity of certain total type structures.
   • Thomas Streicher's book Domain-Theoretic Foundations of Functional Programming, highly recommended.