# Sewon Park: A Dependent Type Theory (under construction) for Multivalued Computation in Computable Analysis

Date: 14. 1. 2020

Source: Mathematics and theoretical computing seminar

Source: Mathematics and theoretical computing seminar

Četrtek, 16. 1. 2020, od 11h do 13h, učilnica 3.07, Jadranska 21

**Abstract: **Multivalued Computation is essential in computable analysis.

For example, deciding a soft-sign of a real number up to some tolerance parameter is necessarily multivalued.

In this talk, a dependent type theory with a primitive type R for abstract real numbers and a type former M for multivaluedness is devised.

A multivalued real function is, therefore, simply a term, in the type theory, of type R -> M R.

The type former can be applied to sigma types as well, thus that multivalued existences and multivalued disjunctions can be expressed in the type theory.

The type theory has a realizability interpretation in the category of assemblies.