Analysis in univalent type theory

Add to your list(s) Download to your calendar using vCal

• Auke Booij, CS Theory Group, Birmingham
• Thursday 14 September 2017, 12:00-13:00
• CS 217.

If you have a question about this talk, please contact Dr Steve Vickers.

Practice talk for the Oberseminar Mathematische Logik in München at Chuangjie’s group.

It is not possible to exhibit information about real numbers such as Dedekind reals or (quotiented) Cauchy reals (as opposed to Bishop-style Cauchy reals), because, for example, there are no non-constant functions into observable types such as the booleans or the integers. We overcome this by considering real numbers that have additional structure, which we call strong locatedness. With this structure, it is possible, for instance, to construct a signed-digit representation or a Cauchy approximation. Such constructions are reminiscent of computable analysis. However, the main point is that instead of working with a notion of computability, we simply work constructively to extract observational information.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Lab Lunch
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.