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

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

Datum objave: 14. 1. 2020
Vir: Seminar za temelje matematike in teoretično računalništvo
Č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.