Sam Sanders: Reuniting the antipodes: bringing together Constructive and Nonstandard Analysis

In the Sixties, Errett Bishop introduced Constructive Analysis, a redevelopment of classical Mathematics based on the fundamental notions of `algorithm' and `proof', inspired by the BHK (Brouwer-Heyting-Kolmogorov) interpretation. Constructive Reverse Mathematics (CRM) is a spin-off from Harvey Friedman's famous `Reverse Mathematics' program, based on Constructive Analysis.

Bishop famously derided Nonstandard Analysis for its lack of computational meaning. In this talk, we introduce `Ω-invariance': a simple and elegant definition of `finite procedure' in (classical) Nonstandard Analysis.  Using an intuitive  nterpretation, we obtain many results from CRM, thus showing that Ω-invariance is quite close to Bishop's notion of algorithm.   We suggest a possible application of Ω-invariance to Per Martin-Löf's famous Type Theory, in light of its recent interpretation using homotopy.