On Formal Verification in Imperative Multivalued Programming over Continuous Data Types. - Norbert Th. Müller; Sewon Park 001; Norbert Preining; Martin Ziegler 001 (CoRR, 2016)

Computable Operations on Compact Subsets of Metric Spaces with Applications to Fréchet Distance and Shape Optimization. - Chansu Park; Ji-won Park; Sewon Park 001; Dongseong Seon; Martin Ziegler 001 (CoRR, 2017)

Computing Periods ... . - Junhee Cho 001; Sewon Park 001; Martin Ziegler 001 (WALCOM, 2018)

Randomized Computation of Continuous Data: Is Brownian Motion Computable? - Willem L. Fouché; Hyunwoo Lee; Donghyun Lim; Sewon Park 001; Matthias Schröder 001; Martin Ziegler 001 (CoRR, 2019)

Axiomatic Reals and Certified Efficient Exact Real Computation. - Michal Konecný; Sewon Park 001; Holger Thies (WoLLIC, 2021)

Continuous Abstract Data Types for Verified Computation. - Sewon Park 001 (Bull. Symb. Log., 2021)

Certified Computation of Nondeterministic Limits. - Michal Konecný; Sewon Park 001; Holger Thies (NFM, 2022)

Verified Exact Real Computation with Nondeterministic Functions and Limits. - Sewon Park 001 (FCT, 2023)

Formalizing Hyperspaces for Extracting Efficient Exact Real Computation. - Michal Konecný; Sewon Park 001; Holger Thies (MFCS, 2023)

A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations. - Sewon Park 001; Holger Thies (ITP, 2024)

An Imperative Language for Verified Exact Real-Number Computation. - Andrej Bauer; Sewon Park 001; Alex Simpson (CoRR, 2024)

Formalizing Hyperspaces and Operations on Subsets of Polish spaces over Abstract Exact Real Numbers. - Michal Konecný; Sewon Park 001; Holger Thies (CoRR, 2024)

Semantics, Specification Logic, and Hoare Logic of Exact Real Computation. - Sewon Park 001; Franz Brauße; Pieter Collins; SunYoung Kim; Michal Konecný; Gyesik Lee; Norbert Th. Müller; Eike Neumann; Norbert Preining; Martin Ziegler 001 (Log. Methods Comput. Sci., 2024)

cAERN library. - Michal Konecný; Sewon Park 001; Holger Thies (DROPS Artifacts, 2024)

Extracting efficient exact real number computation from proofs in constructive type theory. - Michal Konecný; Sewon Park 001; Holger Thies (J. Log. Comput., 2025)