|Ludwig-Maximilians-Universität München||Mathematisches Institut|
|Constructive convex analysis||Josef Berger Gregor Svindland|
|9:45–10:00||J. Berger / G. Svindland||opening|
|10:00–10:45||Klaus Mainzer||Bridging Logic, Mathematics, Computer Science, and Philosophy|
|10:45–11:30||Vasco Brattka||The Computational Content of the Brouwer Fixed Point Theorem Revisited|
|11:30–12:15||Douglas S. Bridges||Boundaries and separation|
|13:45–14:30||Peter M. Schuster||Lindenbaum's Lemma, Syntactically?|
|14:30–15:15||Helmut Schwichtenberg||Logic for exact real arithmetic|
|15:30–16:15||Hajime Ishihara||A constructive proof of the minimax theorem|
|16:15–16:45||Takako Nemoto||Weak König's Lemma for convex trees|
|17:00–17:30||Tatsuji Kawai||The space of located subsets|
|17:30–18:00||Sam Sanders||The crazy Reverse Mathematics of Nonstandard Analysis and Computability Theory|
the space of located subsetsof the continuous lattice. The construction of this point-free space from a continuous lattice extends to a functor that is left adjoint to the forgetful functor from the category KReg of compact regular formal topologies to that of continuous lattices and perfect maps. Thus, the space of located subsets exhibits the Lawson topology on the continuous lattice. As expected, the monad on KReg induced by this functor is isomorphic to the Vietoris moand.
Big Five, which are also linearly ordered. We show that the counterparts of the Big Five (and other systems) in Nonstandard Analysis behave very differently. These results are obtained via (and often reformulations of) results in higher-order computability theory. As an example, the nonstandard counterpart of WKL behaves like Kohlenbach’s generalisation of WKL, but with nonstandard continuity instead of the epsilon-delta variety.