Sewon Park (박세원)
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,
formalization of constructive, computable, and classical mathematics in a dependent type theory and in 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
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 )
28 August 2017 – 20 August 2021
M.S. at KAIST School of Computing in Computer Science
B.S. at KAIST in Physics (main major) and Industrial System Engineering (double major)
Publications
The authors in all my contributions except one marked with * are written in the alphabetical order
Journals
*
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
Extracting efficient exact real number computation from proofs in constructive type theory (2022;
accepted )
Michal Konečný, Sewon Park, and Holger Thies
Oxford University Press – Journal of Logic and Computation (JLC )
Manuscript
An Imperative Language for Verified Exact Real-Number Computation (2024;
submitted )
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)
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
Show more (-2020)
Compact Subsets in Exact Real Computation (2020)
Topological Aspects on Nondetermistic Computation (2020)
Grassmannian as Continuous Data Type with Computable Semantics (2019)
Seokbin Lee, Donghyun Lim, Sewon Park, Martin Ziegler
한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), pp. 1767-1769
Tensor Calculus in Exact Real Computation on Simplicial Complexes (2018)
Chansu Park, Sewon Park, Martin Ziegler
한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), pp. 1729-1731
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
Abstract data type for exact real numbers and verified computation Slides
Verified computation over real numbers and other continuous objects
Toward verified real computation
Contributed Talks
Verifying iRRAM-like implementation of exact real computation
Verified Exact Real Computation with Nondeterministic Functions and Limits
Towards verified implementation of iterative and interactive real-RAM
Show more (-2022)
A type-theoretical interpretation of intuitionistic fixed point logic
Ulrich Berger, Sewon Park, Holger Thies, Hideki Tsuiki
2022 Global KMS International Conference
KMS 2022
Oct 18 – 21, 2022, Seoul, Korea (online talk)
Some steps toward program extraction in a type-theoretical interpretation of IFP
Ulrich Berger, Sewon Park, Holger Thies, Hideki Tsuiki
Continuity, Computability, Constructivity - From Logic to Algorithms
CCC 2022
Sep 19 – 23, 2022, Padova, Italy
Nondeterministic limits and certified exact real computation
Michal Konečný, Sewon Park, Holger Thies
Nineteenth International Conference on Computability and Complexity in Analysis
CCA 2022
May 23 – 26, 2022, Glenside (PA), USA (online talk)
An axiomatization of real numbers in constructive type theory and its application
Michal Konečný, Sewon Park, Holger Thies
2022 China-South Korea Non-Classical Logics and Related Algebra Systems Academic Seminar
Feb 12 – 13, 2022, Online
Lazy Data Types
Jihoon Hyun, Sewon Park, Martin Ziegler
The 14th Annual Meeting of the Asian Association for Algorithms and Computation
AAAC 2021
Oct 22 – 24, 2021, Tainan, Taiwan (online talk)
Nondeterminism in constructive metric completeness
Michal Konečný, Sewon Park, Holger Thies
2021 KMS Annual Meeting Special Session: Mathematical Logic and Its Applications
KMS Fall 2021
Oct 20 – 22, 2021, Online
Intuitionistic Logic, Type Theory, and Computer Science
Topological Aspects on Nondetermistic Computation
Clerical: an Imperative Language for Verified Real-number Computation
Andrej Bauer, Sewon Park, Alex Simpson
Seventeenth International Conference on Computability and Complexity in Analysis
CCA 2020
Sep 09 – 11, 2020, Online
Multivalued functions in a dependent type theory
Andrej Bauer, Philipp G., Sewon Park, Egbert Rijke
KMS Spring 2020 - Special Session: Mathematical Logic and Its Applications
KMS Spring 2020
Jul 03 – 03, 2020, Online
Axiomatic Reals in Type Theory for Program Extraction
Interval Gaussian Algorithm for Singular Interval Matrices
Sewon Park
Fall Workshop on Algorithms and Computation
FWAC 2018
Nov 2018, Seoul, Korea
Interval Gaussian Algorithm for Singular Interval Matrices
Sewon Park
The 18th International Symposium on Scientific Computing, Computer Arithmetic, and Verified Numerical Computations
SCAN 2018
Sep 2018, Tokyo, Japan
Reliable Diagonalization of Degenerate Matrices
Implementation and Empirical Evaluation of two Algorithms for Computing Characteristic Polynomials' Coefficients in Exact Real Arithmetic
Sewon Park
Fall Workshop on Algorithms and Computation
FWAC 2016
Nov 2016, Seoul, Korea
Verification in Real Computation
Norbert Th., Sewon Park, Norbert Preining, Martin Ziegler
The 19th Japan-Korea Joint Workshop on Algorithms and Computation
WAAC 2016
Aug 2016, Hakodate, Japan
On Formal Verification in Imperative Multivalued Programming over Continuous Data Types
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
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
Autumn School Proof and Computation PC18
University of Trier
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 )
Coq-clerical: Clerical Coq Formalization (
Coq Proof Assistant )
Clerical: Command-like expressions for infinite-precision calculations (
OCaml )
iRRAMx: an extension of iRRAM (
C++ )
Jiman Hwang, Jihoon Hyun, Hyunwoo Lee, Donghyun Lim, Sewon Park, Holger Thies and Martin Ziegler
Other Activities
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
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
The first Korea Logic Day 2021 KLD2021
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
sewon_park.txt · Last modified: 2024/10/02 14:36 by sewon
Page Tools