Proof, Computation, Complexity 2016

Dag Normann, Univ. of Oslo, Norway: Revisiting Transfinite Types

In this talk I will reconstruct spaces of countable and uncountable transfinite types, this time using limit spaces. This approach turns out to give a better access to internal concepts of computability for such spaces.
The talk will be a report on ongoing research. This research is rooted in earlier work by Ulrich Berger and by myself, and the revisiting is inspired by recent contributions by Selivanov, Schröder and de Brecht.

Paulo Oliva, Queen Mary Univ. London, UK: Modified bar recursion - 15 years on

I remember as if it was yesterday when during the second year (2001) of my PhD studies we had a visitor giving a talk about “modified bar recursion”. I had just learnt about Spector bar recursion from Kohlenbach and was quite intrigued by what kind of different form of bar recursion one could come up with. The speaker was Ulrich Berger, and that talk would shape much of what I have been doing since then. I went on to visit Ulrich in Swansea, and had the honour to co-author two papers [1,2] with him on this new form of bar recursion. In this talk I hope to look back at that work, and much of what followed, in terms of inter-definability results [3] and novel connections to Game Theory via the recent work on selection functions [4,5].

[1] Ulrich Berger and Paulo Oliva, Modified bar recursion, MSCS, 16(2):163-183, 2006
[2] Ulrich Berger and Paulo Oliva, Modified bar recursion and classical dependent choice, LNL, 20:89-107, 2005
[3] Thomas Powell, The equivalence of bar recursion and open recursion, APAL, 165(11):1727-1754, 2014
[4] Martín Escardó and Paulo Oliva, Bar recursion and products of selection functions, JSL, 80(1):1-28, 2015
[5] Martín Escardó and Paulo Oliva, Sequential games and optimal strategies, Proc. of the Royal Society A, 467:1519-1545, 2011

Thomas Streicher, Technical University Darmstadt, Germany: An effective Spectral Theorem for bounded self adjoint operators

Using (sort of) abstract methods from topological domain theory we prove that the spectral theorem for bounded selfadjoint operators is effective in the sense of TTE, i.e., it holds in the Kleene Vesley topos. We also identify the natural topology on the involved spaces induced by their effective representations.

Page maintained by:

Last modified (date in French): dim. mai 1 21:39:10 CEST 2016