I am a JSPS International Research Fellow hosted by Prof. Akitoshi Kawamura at the Research Institute for Mathematical Sciences, Kyoto University. You may contact me by Sewon@sewonpark.com or sewon@kurims.kyoto-u.ac.jp.

My old KAIST email address sewon[at]kaist.ac.kr is now deactivated. If you have sent any email to the deactivated email address, please send it again to another address above.

• Constructive mathematics
• Type theories and their interpretations
• Computability and complexity in analysis
• Certified / Verified exact real number computation
• Programming language theory
• Drawing..

• JSPS International Research Fellow
  • Supported by JSPS Postdoctoral Fellowship for Research in Japan(Standard)
  • on “Verified Exact Computation over Continuous Higher Types”
  • Research Institute for Mathematical Sciences, Kyoto University, Japan
  • 1 April 2022 - 31 March 2024
• Postdoctoral researcher
  • Research Institute for Mathematical Sciences, Kyoto University, Japan
  • 16 October 2021 - 31 March 2022

• KAIST, Daejeon, Korea
  • PhD. in Computer Science
    • Complexity and Real Computation Laboratory, School of Computing
    • dissertation: Continuous Abstract Data Types for Verified Computation
      • 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. in Computer Science
    • Complexity and Real Computation Laboratory, School of Computing
    • dissertation: Verified Real Computation
    • 31 August 2015 – 18 August 2017
  • B.S. in Physics (main major) and Industrial System Engineering (double marjor)
    • 7 February 2011 – 14 August 2015

See DBLP

• “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.
  • https://doi.org/10.1007/978-3-031-06773-0_41
• “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
  • https://doi.org/10.1007/978-3-030-88853-4_16
• “Compact Subsets in Exact Real Computation” (2020)
  • Sewon Park and Jiman Hwang
  • 한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), pp. 1104-1106
  • https://www.dbpia.co.kr/journal/articleDetail?nodeId=NODE10529900
• “Topological Aspects on Nondetermistic Computation” (2020)
  • Donghyun Lim and Sewon Park
  • 한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), pp. 1107-1108
  • https://www.dbpia.co.kr/journal/articleDetail?nodeId=NODE10529901
• “Grassmannian as Continuous Data Type with Computable Semantics” (2019)
  • Seokbin Lee, Donghyun Lim, Sewon Park, Martin Ziegler
  • 한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), pp. 1767-1769
  • https://www.dbpia.co.kr/journal/articleDetail?nodeId=NODE09302066
• “Tensor Calculus in Exact Real Computation on Simplicial Complexes” (2018)
  • Chansu Park, Sewon Park, Martin Ziegler
  • 한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), pp. 1729-1731
  • https://www.dbpia.co.kr/journal/articleDetail?nodeId=NODE07503476
• “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
  • https://doi.org/10.1007/978-3-319-75172-6_12

• “Extracting efficient exact real number computation from proofs in constructive type theory” (2022, submitted)
  • Michal Konečný, Sewon Park, and Holger Thies
  • https://arxiv.org/abs/2202.00891
• “Randomized Computation of Continuous Data: Is Brownian Motion Computable?” (2019)
  • Fouché, Willem, Hyunwoo Lee, Donghyun Lim, Sewon Park, Matthias Schröder, and Martin Ziegler
  • https://arxiv.org/abs/1906.06684v1
• “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
  • https://arxiv.org/abs/1701.08402v2
• “Foundation of Computer (Algebra) ANALYSIS Systems: Semantics, Logic, Programming, Verification” (2016, submitted)
  • Sewon Park, Franz Brauße, Pieter Collins, SunYoung Kim, Michal Konečný, Gyesik Lee, Norbert Müller, Eike Neumann, Norbert Preining, and Martin Ziegler
  • https://arxiv.org/abs/1608.05787v5

• “ A type-theoretical interpretation of intuitionistic fixed point logic”
  • joint work with Ulrich Berger, Holger Thies and Hideki Tsuiki
  • 2022 Global KMS International Conference KMS2022 Fall
  • October 18–21, 2022, Seoul, Korea (Online) (talk on 19th)
• “Some steps toward program extraction in a type-theoretical interpretation of IFP”
  • joint work with Ulrich Berger, Holger Thies and Hideki Tsuiki
  • Continuity, Computability, Constructivity - From Logic to Algorithms CCC2022
  • September 19–23, 2022, Padova, Italy (talk on 20th)
• “Nondeterministic limits and certified exact real computation”
  • joint work with Michal Konečný and Holger Thies
  • Nineteenth International Conference on Computability and Complexity in Analysis CCA2022
  • May 23-26, 2022, Online (talk on 23rd)
  • Slides
• “Verified computation over real numbers and other continuous objects” (tutorial)
  • The second Japan-Russia workshop on effective descriptive set theory, computable analysis and automata link
  • March 2-4, 2022, Akita, Japan (talk on 2nd and 3rd)
  • Slides 1 and Slides 2.
• “An axiomatization of real numbers in constructive type theory and its application”
  • (based on) joint work with Michal Konečný and Holger Thies
  • 2022 China-South Korea Non-Classical Logics and Related Algebra Systems Academic Seminar
  • February 12-13, 2022, Online (talk on 12th)
  • Slides
• “Lazy Data Types”
  • joint work with Jihoon Hyun and Martin Ziegler
  • The 14th Annual Meeting of the Asian Association for Algorithms and Computation AAAC2021
  • October 24, 2021, Airmeet online meeting
• “Nondeterminism in constructive metric completeness” abstract
  • joint work with Michal Konečný and Holger Thies
  • 2021 KMS Annual Meeting Special Session: Mathematical Logic and Its Applications KMS2021
  • October 21, 2021, Zoom Online Meeting
• “Toward verified real computation” (invited talk)
  • Continuity, Computability, Constructivity From Logic to Algorithms CCC2021
  • September 23, 2021, Zoom Online Meeting
• “Intuitionistic Logic, Type Theory, and Computer Science” (introductory)
  • the first Korea Logic Day 2021 KLD2021
  • January 14, 2021, Zoom Online Meeting
• “Topological Aspects on Nondetermistic Computation”
  • joint work with Donghyun Lim
  • Korea Software Congress 2020 KSC2020
  • December 2020, Zoom Online Meeting
• “Clerical: an Imperative Language for Verified Real-number Computation”
  • joint work with Andrej Bauer and Alex Simpson
  • Seventeenth International Conference on Computability and Complexity in Analysis CCA2020
  • September 2020, Zoom Online Meeting
• “Multivalued functions in a dependent type theory” abstract
  • joint work with Andrej Bauer, Philipp G. Haselwarter, and Egbert Rijke
  • Special Session: Mathematical Logic and Its Applications KMS Spring 2020
  • July 2020, Zoom Online Meeting
• “Axiomatic Reals in Type Theory for Program Extraction”
  • Computability, Continuity, Constructivity - from Logic to Algorithms CCC2019
  • September 2019, Ljubljana, Slovenia
• “Interval Gaussian Algorithm for Singular Interval Matrices”
  • Fall Workshop on Algorithms and Computation FWAC2018
  • November 2018, Seoul, Korea
• “Interval Gaussian Algorithm for Singular Interval Matrices”
  • The 18th International Symposium on Scientific Computing, Computer Arithmetic, and Verified Numerical Computations SCAN2018
  • September 2018, Tokyo, Japan
• “Reliable Diagonalization of Degenerate Matrices”
  • joint work with Martin Ziegler
  • Computability and Complexity in Analysis 2017 CCA2017
  • July 2017, Daejeon, Korea
• “Implementation and Empirical Evaluation of two Algorithms for Computing Characteristic Polynomials' Coefficients in Exact Real Arithmetic”
  • Fall Workshop on Algorithms and Computation FWAC2016
  • November 2016, Seoul, Korea
• “Verification in Real Computation”
  • joint work with Norbert Th. Müller, Norbert Preining and Martin Ziegler
  • The 19th Japan-Korea Joint Workshop on Algorithms and Computation WAAC2016
  • August 2016, Hakodate, Japan
• “On Formal Verification in Imperative Multivalued Programming over Continuous Data Types”
  • joint work with Norbert Th. Müller, Norbert Preining and Martin Ziegler
  • Computability and Complexity in Analysis 2016 CCA2016
  • June 2016, Faro, Portugal

• University of Ljubljana
  • Prof. Alex Simpson
  • February 27 – March 15, 2023, Ljubljana, Slovenia
• University of Ljubljana
  • Prof. Alex Simpson
  • 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
  • October – November, 2017, Ljubljana, Slovenia

• 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, 2018, Daejeon, Korea
• Computability and Complexity in Analysis 2017 CCA2017
  • Organizing committee member
  • July 24-27, 2017, Daejeon, Korea

• cAERN
• iRRAMx
• iRRAM-Random
• irram.sh
• erlc-js

CID

Junhee Cho / Akitoshi Kawamura / Junguk Lee / Donghyun Lim / Florian Steinberg / Holger Thies / Chuangjie Xu / Martin Ziegler