Table of Contents
Sewon Park (박세원)
English | 日本語
DBLP ・ GitHub ・ Google Scholar ・ LinkedIn ・ ORCID ・ Research Map
* none of the above profiles is being actively maintained. Only this webpage is ☺︎
I am a postdoctoral researcher hosted by Prof. Atsushi Igarashi at the Computer Software Group, Kyoto University. You may contact me by Sewon@sewonpark.com or by sewon@fos.kuis.kyoto-u.ac.jp.
My research interests include computable analysis, verified exact real-number computation, and formalization of constructive, computable, and classical mathematics in a dependent type theory and its implementation, such as the Coq proof assistant.
This webpage works as my CV when it is printed out. Including boxes like this, unnecessary stuff will disappear in printing.
I started to post some notes in Notes. Take a look!
Employment
-
Postdoctoral Researcher
-
Graduate School of Informatics, Kyoto University, Japan (hosted by Prof. Atsushi Igarashi)
-
1 April 2024 – current
Postdoctoral Researcher-
Research Institute for Mathematical Sciences, Kyoto University, Japan (hosted by Prof. Akitoshi Kawamura)
-
16 October 2021 – 31 March 2024 (1 April 2022 – 31 March 2024 was supported by JSPS Postdoctoral Fellowship)
Education
-
PhD at KAIST School of Computing (Daejeon, South Korea) in Computer Science
-
Dissertation: Continuous Abstract Data Types for Verified Computation (supervised by Prof. Martin Ziegler)
-
The abstract published in The Bulletin of Symbolic Logic, 27(4), 531-531. doi:10.1017/bsl.2021.51
28 August 2017 – 20 August 2021M.S. at KAIST School of Computing in Computer Science-
Thesis: Verified Real Computation (supervised by Prof. Martin Ziegler)
-
31 August 2015 – 18 August 2017
B.S. at KAIST in Physics (main major) and Industrial System Engineering (double major)-
7 February 2011 – 14 August 2015
Publications
The authors in all my contributions except one marked with ⭐︎ are listed in the alphabetical order
Journals
-
Extracting efficient exact real number computation from proofs in constructive type theory (2024)
-
Michal Konečný, Sewon Park, and Holger Thies
-
Oxford University Press – Journal of Logic and Computation (JLC), published online in advance in October 2024
-
Preprint available at https://arxiv.org/abs/2202.00891
⭐︎Semantics, Specification Logic, and Hoare Logic of Exact Real Computation (2024)-
Sewon Park, Franz Brauße, Pieter Collins, SunYoung Kim, Michal Konečný, Gyesik Lee, Norbert Müller, Eike Neumann, Norbert Preining, and Martin Ziegler
-
Logical Methods in Computer Science (LMCS), June 24, 2024, Volume 20, Issue 2
Manuscript
-
Formalizing Hyperspaces and Operations on Subsets of Polish spaces over Abstract Exact Real Numbers (2024; submitted)
-
Michal Konečný, Sewon Park, and Holger Thies
-
Preprint available at: https://arxiv.org/abs/2410.13508
An Imperative Language for Verified Exact Real-Number Computation (2024; submitted)-
Andrej Bauer, Sewon Park, and Alex Simpson
-
Preprint available at: https://arxiv.org/abs/2409.11946
Refereed International Conference Publications
-
A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations (2024)
-
Sewon Park and Holger Thies
-
In: Bertot, Y. and Kutsia, T. and Norrish, M. (eds) 15th International Conference on Interactive Theorem Proving. ITP 2024
-
Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Verified Exact Real Computation with Nondeterministic Functions and Limits (2023)-
Sewon Park
-
In: Fernau, H., Jansen, K. (eds) Fundamentals of Computation Theory FCT 2023
-
Lecture Notes in Computer Science, vol 14292. Springer, Cham.
Formalizing Hyperspaces for Extracting Efficient Exact Real Computation (2023)-
Michal Konečný, Sewon Park, and Holger Thies
-
In: Leroux, J., Lombardy, S., Peleg, D. (eds) 48th International Symposium on Mathematical Foundations of Computer Science. MFCS 2023
-
Leibniz International Proceedings in Informatics (LIPIcs), vol 272. Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Certified Computation of Nondeterministic Limits (2022)-
Michal Konečný, Sewon Park, and Holger Thies
-
In: Deshmukh, J.V., Havelund, K., Perez, I. (eds) NASA Formal Methods. NFM 2022
-
Lecture Notes in Computer Science, vol 13260. Springer, Cham.
Axiomatic Reals and Certified Efficient Exact Real Computation (2021)-
Michal Konečný, Sewon Park, and Holger Thies
-
In: Silva A., Wassermann R., de Queiroz R. (eds) Logic, Language, Information, and Computation. WoLLIC 2021
-
Lecture Notes in Computer Science, vol 13038. Springer, Cham
Computing Periods … (2018)-
Junhee Cho, Sewon Park, and Martin Ziegler
-
In: Rahman M., Sung WK., Uehara R. (eds) WALCOM: Algorithms and Computation. WALCOM 2018
-
Lecture Notes in Computer Science, vol 10755. Springer, Cham
Preprints
-
Randomized Computation of Continuous Data: Is Brownian Motion Computable? (2019)
-
Fouché, Willem, Hyunwoo Lee, Donghyun Lim, Sewon Park, Matthias Schröder, and Martin Ziegler
Computable Operations on Compact Subsets of Metric Spaces with Applications to Fr\’echet Distance and Shape Optimization (2017)-
Chansu Park, Ji-Won Park, Sewon Park, Dongseong Seon, and Martin Ziegler
Short Peer-reviewed Conference Proceedings
-
-
-
-
-
-
-