What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common.


This is a tutorial paper by Martin Escardo and Paulo Oliva, to appear in MSFP 2010, ACM SIGPLAN Mathematically Structured Functional Programming, ACM Press.
  1. The tutorial paper: What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common.

    We would have liked to include more material and more remarks of an expository nature, and more references to other people's related work, but we had a hard limit of 12 pages.

  2. Haskell programs.

  3. Agda programs/proofs.

    Set your browser to use UTF-8 encoding to be able to properly see the mathematical symbols.

  4. Zip file with the Haskell and Agda programs.

  5. A Haskell program showing that non-empty exhaustible sets are searchable.

    (This was mentioned in the paper but omitted for lack of space.)

  6. See also the related posts Seemingly impossible functional programs. and A Haskell monad for infinite search in finite time at Andrej Bauer's blog Mathematics and Computation.

    Functional programmers with less mathematical background should probably start from those posts.

  7. Errata, last updated 12 August 2010 3:38pm BST.

    The Corrected version of the paper as documented in the errata.


Martin Escardo
m.escardo@cs.bham.ac.uk
Last modified: Thu Aug 12 15:38:28 BST 2010