University of Birmingham > Talks@bham > Lab Lunch > What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.