Time:  12  1:20 p.m. 
Room: 
CFA 110

Speaker:  Henry Towsner Graduate Student in Mathematical Sciences Carnegie Mellon University 
Title: 
A Realizability Interpretation for Classical Analysis

Abstract: 
I present a realizability interpretation of classical
analysis, that is, a method of assigning to proofs in second order
arithmetic an object (in this case functionals of the polymorphic
lambda calculus) in such a way that the object assigned to a formula
\exists x A(x) (where A is recursive) is a number n so that A(n)
holds. In addition, the object assigned to a formula \forall x\exists
y A(x,y) (where A is recursive) will be a type one functional f such
that f(n)=m iff m is the least y satisfying A(n,y).

Organizer's note:  Please bring your lunch.
