−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 2021
-
-
M.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
Conference Talks
These are lists automatically generated from my .bib database. (To be precise, it automatically generates the lists in here where I copy these lists from.) There, also a list of conference contributions that I coauthored can also be found.
Invited Talks
-
Verified computation over real numbers and other continuous objects
-
The second Japan-Russia workshop on effective descriptive set theory, computable analysis and automata Link
-
Mar 02 – 04, 2022, Akita, Japan
-
-
Toward verified real computation
-
Continuity, Computability, Constructivity From Logic to Algorithms CCC 2021
-
Sep 20 – 24, 2021, Online
-
Contributed Talks
-
Verifying iRRAM-like implementation of exact real computation
-
Sewon Park, Holger Thies
-
Continuity, Computability, Constructivity - From Logic to Algorithms CCC 2023
-
Sep 25 – 29, 2023, Kyoto, Japan
-
-
Verified Exact Real Computation with Nondeterministic Functions and Limits
-
Sewon Park
-
24th International Symposium on Fundamentals of Computation Theory FCT 2023
-
Sep 18 – 21, 2023, Trier, Germany (online talk)
-
-
Towards verified implementation of iterative and interactive real-RAM
-
Sewon Park, Holger Thies
-
Twentieth International Conference on Computability and Complexity in Analysis CCA 2023
-
Sep 07 – 09, 2023, Dubrovnik, Croatia
-
Research Visits
-
Korean Mathematical Society 2024 Spring meeting and KAIST
-
April 17 – 21, 2024, Daejeon Convention Center and KAIST, Daejeon, Korea
-
-
数学基礎論サマースクール2023 link
-
September 11 – 15, 2023, Meiji University, Tokyo, Japan
-
-
Laboratoire d'informatique de l'École polytechnique
-
Prof. Olivier Bournez
-
September 4 – 6, 2023, Palaiseau, France
-
-
University of Ljubljana
-
Prof. Alex Simpson and Prof. Andrej Bauer
-
February 27 – March 15, 2023, Ljubljana, Slovenia
-
-
Meiji University(明治大学)
-
Prof. Kenshi Miyabe(宮部賢志)
-
February 14 – 17, 2023, Kanagawa, Japan
-
-
University of Ljubljana
-
Prof. Alex Simpson and Prof. Andrej Bauer
-
January – February, 2020, Ljubljana, Slovenia
-
-
Autumn School Proof and Computation PC19
-
September 2019, Herrsching, Germany
-
-
Autumn School Proof and Computation PC18
-
September 2018, Fischbachau, Germany
-
-
University of Trier
-
Prof. Norbert Müller
-
November – December, 2017, Trier, Germany
-
-
Dagstuhl Seminar 17481 Reliable Computation and Complexity on the Reals
-
November 26 – December 1, 2017, Schloss Dagstuhl, Wadern, Germany
-
-
University of Ljubljana
-
Prof. Alex Simpson and Prof. Andrej Bauer
-
October – November, 2017, Ljubljana, Slovenia
-
Software
-
CAern: Axiomatic Reals and Certified Efficient Exact Real Computation (Coq Proof Assistant)
-
Michal Konečný, Sewon Park and Holger Thies,
-
-
Coq-clerical: Clerical Coq Formalization (Coq Proof Assistant)
-
Andrej Bauer and Sewon Park
-
-
Clerical: Command-like expressions for infinite-precision calculations (OCaml)
-
Andrej Bauer and Sewon Park
-
-
iRRAMx: an extension of iRRAM (C++)
-
Jiman Hwang, Jihoon Hyun, Hyunwoo Lee, Donghyun Lim, Sewon Park, Holger Thies and Martin Ziegler
-
-
iRRAM-Random (C++)
-
Sewon Park
-
Other Activities
-
Computability and Complexity in Analysis 2025 CCA2025
-
Organizing Committee member
-
September 23-26 (to be confirmed), 2025, Kyoto, Japan
-
-
The Fourth Korea Logic Day 2025 KLD2025
-
Organizing Committee member
-
January 13-15, 2025, Changwon, Korea
-
-
2024 Continuity, Computability, Constructivity - From Logic to Algorithms CCC2024
-
Programme Committee member
-
October 2-4, 2024, Nice, France
-
-
The third Korea Logic Day 2024 KLD2024
-
Organizing Committee member
-
12 January 2024, online
-
-
2023 Continuity, Computability, Constructivity - From Logic to Algorithms CCC2023
-
Programme Committee and Organizing Committee member
-
September 25 - 29, 2023, Kyoto, Japan
-
-
The second Korea Logic Day 2022 KLD2022
-
Organizing Committee member
-
14 January 2022, online
-
-
The first Korea Logic Day 2021 KLD2021
-
Organizing Committee member
-
14 January 2021, online
-
-
The 22nd Japan-Korea Joint Workshop on Algorithms and Computation WAAC2019
-
Organizing Committee member
-
October 4-5, 2019, Daejeon, Korea
-
-
Computability and Complexity in Analysis 2017 CCA2017
-
Organizing Committee member
-
July 24-27, 2017, Daejeon, Korea
-
Links
CID ・ Korea Logic Day ・ Andrej Bauer ・ Junhee Cho ・ Akitoshi Kawamura ・ Junguk Lee ・ Donghyun Lim ・ Florian Steinberg ・ Holger Thies ・ Chuangjie Xu ・ Martin Ziegler