https://sewonpark.com/ 2026-05-16T14:40:08+00:00 https://sewonpark.com/ https://sewonpark.com/_media/wiki/logo.png text/html 2022-01-23T06:46:13+00:00 Anonymous (anonymous@undisclosed.example.com) https://sewonpark.com/abstract/multivalued_functions_dependent_type_theory?rev=1642920373&do=diff Multivalued functions in a dependent type theory Andrej Bauer, Philipp G. Haselwarter, Sewon Park, Egbert Rijke<https://www.kms.or.kr/conference/abstract/search_view.html?num=7324&uid=57&start=0&sort=sortDate&period=57&cate=&etitle=&key_word=&au_name=&au_ename=Sewon%20park&au_office=&au_eoffice=&mode=search&section=> text/html 2022-01-23T06:39:34+00:00 Anonymous (anonymous@undisclosed.example.com) https://sewonpark.com/abstract/nondeterminism_in_constructive_metric_completeness?rev=1642919974&do=diff Nondeterminism in constructive metric completeness Michal Konečný (Aston University, UK), Sewon Park (KAIST, Korea), Holger Thies (Kyoto University, Japan) The computational content of constructive metric completeness is the operator that computes limits of Cauchy sequences. Using it, we can construct certified programs that compute interesting transcendental real numbers from sequences of approximations. The desired nondeterministic version of it would be to nondeterministically compute real nu…