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.
Please consider subscribing to the Korea Logic Mailing List to stay informed about various logic-related events in Korea!
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
-
-
-
-
-
-
-