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

Add to your list(s) Download to your calendar using vCal

• Martin Escardo
• Tuesday 12 October 2010, 12:00-13:00
• CS 124.

If you have a question about this talk, please contact Dan Ghica.

Much of this is joint work with Paulo Oliva (Queen Mary).

Abstract. I discuss a higher-type functional, written in the functional programming language Haskell in the talk, which:

(1) Optimally plays sequential games.

(2) Implements a computational version of the Tychonoff Theorem from
    topology.

(In particular, this shows that certain function types actually
do have decidable equality, contrary to popular belief.)

(3) realizes the Double-Negation Shift from logic and proof theory

(This allows to computationally extract witnesses from classical
proofs that use the axiom of countable (dependent) choice).

I will run this program in the talk (and show you Agda code for (3)).

REMARK . Some of you have seen bits and pieces of this in the last three years or so. Here I put everything together in a single talk, and make it more practically oriented. This is based on an invited talk I gave at MSFP (mathematically structured functional programming).

We produced a tutorial paper based on several papers we wrote (jointly and otherwise), with the title of this talk:

http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/Escardo-Oliva-MSFP2010-corrected.pdf

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 124
• Lab Lunch

Note that ex-directory lists are not shown.