Sewon's Blog
About erlc-js Gallery
  • Grid: add grids on your pictures!
  • Erlc: execute your exact real arithmetic program online!
  • Chinese vocabulary: online vocabulary quiz.
  • Name: Sewon Park
  • Interests:
    • Constructive Mathematics
    • Type theories and their interpretations
    • Computability and Complexity in Analysis
    • Programming language theory
    • Drawing..
  • Email: swelite@kaist.ac.kr
  • Education:
    • KAIST, Daejeon, S. Korea
      • PhD. in Computer Science, Complexity and Real Computation Laboratory, School of Computing, August 2021 (expected)
      • M.S. in Computer Science, Complexity and Real Computation Laboratory, School of Computing, August 2017
        • dissertation: Verified Real Computation (pdf)
      • B.S. Physics (main major), Industrial System Engineering (double marjor), August 2015
  • Publications (see DBLP)
    • Sewon Park and Donghyun Lim. “Compact Subsets in Exact Real Computation” (2020). 한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), to be printed.
    • Donghyun Lim and Sewon Park. “Topological Aspects on Nondetermistic Computation” (2020). 한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), to be printed.
    • Fouché, Willem, Hyunwoo Lee, Donghyun Lim, Sewon Park, Matthias Schröder, and Martin Ziegler. “Randomized Computation of Continuous Data: Is Brownian Motion Computable?” (June 16, 2019). https://arxiv.org/abs/1906.06684v1.
    • Seokbin Lee, Donghyun Lim, Sewon Park, Martin Ziegler. “Grassmannian as Continuous Data Type with Computable Semantics” (2019). 한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), 1767-1769. https://www.dbpia.co.kr/journal/articleDetail?nodeId=NODE09302066
    • Chansu Park, Sewon Park, Martin Ziegler. “Tensor Calculus in Exact Real Computation on Simplicial Complexes” (2018). 한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), 1729-1731. https://www.dbpia.co.kr/journal/articleDetail?nodeId=NODE07503476
    • Junhee Cho, Sewon Park, and Martin Ziegler. “Computing Periods …” (2018). 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
    • Chansu Park, Ji-Won Park, Sewon Park, Dongseong Seon, and Martin Ziegler. “Computable Operations on Compact Subsets of Metric Spaces with Applications to Fr\’echet Distance and Shape Optimization” (2017). https://arxiv.org/abs/1701.08402v2.
    • Sewon Park, Franz Brauße, Pieter Collins, SunYoung Kim, Michal Konečný, Gyesik Lee, Norbert Müller, Eike Neumann, Norbert Preining, and Martin Ziegler. “Foundation of Computer (Algebra) ANALYSIS Systems: Semantics, Logic, Programming, Verification” (2016). https://arxiv.org/abs/1608.05787v5.
  • Conference talks:
    • KLD2021 / January 2021 / Zoom Online Meeting / the first Korea Logic Day 2021 / “Intuitionistic Logic, Type Theory, and Computer Science” (tutorial)
    • KSC2020 / December 2020 / Zoom Online Meeting / Korea Software Congress 2020 / “Topological Aspects on Nondetermistic Computation” / joint work with Donghyun Lim
    • CCA2020 / September 2020 / Zoom Online Meeting / Seventeenth International Conference on Computability and Complexity in Analysis / “Clerical: an Imperative Language for Verified Real-number Computation” / joint work with Andrej Bauer, and Alex Simpson
    • KMS Spring 2020 / July 2020 / Zoom Online Meeting / Special Session: Mathematical Logic and Its Applications / “Multivalued functions in a dependent type theory” / joint work with Andrej Bauer, Philipp G. Haselwarter, and Egbert Rijke
    • CCC2019 / September 2019 / Ljubljana, Slovenia / Computability, Continuity, Constructivity - from Logic to Algorithms / “Axiomatic Reals in Type Theory for Program Extraction”
    • FWAC2018 / November 2018 / Seoul, Korea / Fall Workshop on Algorithms and Computation / “Interval Gaussian Algorithm for Singular Interval Matrices”
    • SCAN2018 / September 2018 / Tokyo, Japan / The 18th International Symposium on Scientific Computing, Computer Arithmetic, and Verified Numerical Computations / “Interval Gaussian Algorithm for Singular Interval Matrices”
    • CCA2017 / July 2017 / Daejeon, Korea / Computability and Complexity in Analysis 2017 / “Reliable Diagonalization of Degenerate Matrices” / joint work with Martin Ziegler
    • FWAC2016 / November 2016 / Seoul, Korea / Fall Workshop on Algorithms and Computation / “Implementation and Empirical Evaluation of two Algorithms for Computing Characteristic Polynomials’ Coefficients in Exact Real Arithmetic”
    • WAAC2016 / August 2016 / Hakodate, Japan / The 19th Japan-Korea Joint Workshop on Algorithms and Computation / “Verification in Real Computation” / joint work with Norbert Th. Müller, Norbert Preining and Martin Ziegler
    • CCA2016 / June 2016 / Faro, Portugal / Computability and Complexity in Analysis 2016 / “On Formal Verification in Imperative Multivalued Programming over Continuous Data Types” / joint work with Norbert Th. Müller, Norbert Preining and Martin Ziegler
  • Seminar talks:
    • KAIST Lab Seminar / 2020.05.21 / Classical Types in a Constructive Type Theory and a Transfer Principle for Classical Proofs
    • KAIST Lab Seminar / 2020.03.13 / Constructing Real Numbers
    • KAIST Lab Seminar / 2020.02.13 / A dependent type theory for multivalued computation in computable analysis and its realizability interpretation
    • University of Ljubljana FMF Seminar / 2020.01.14 /A Dependent Type Theory (under construction) for Multivalued Computation in Computable Analysis
    • KAIST Lab Seminar / 2019.06.21 / Axiomatic Exact Real Numbers in Type Theory and Program Extraction
    • KAIST Mini-Workshop / 2019.05.16 / Type Theory with Abstract Reals
    • KAIST Lab Seminar / 2018.11.30 / ERA program extraction from a proof using abstract types
    • KAIST Lab Seminar / 2018.05.16 / Interval Gaussian Algorithm for Singular Interval Matrices
    • University of Ljubljana FMF Seminar / 2017.10.24 / Formal Verification in Imperative Multivalued Programming over Continuous Data Types
    • KAIST Lab Seminar / 2017.09.21 / Formal Verification in Imperative Multivalued Programming over Continuous Data Types
    • KAIST Lab Seminar / 2017.04.21 / On Verified Real Computation
    • KAIST Lab Seminar / 2017.03.06 / Reliable Degenerate Matrix Diagonalization
    • KAML Seminar / 2016.11.04 / Verification in Real Computation
    • KAIST Lab Seminar / 2016.09.26 / Root Clustering Problem of Analytic functions
  • Visits:
    • January 2020 – February 2020: visited Prof. Alex Simpson and Foundations of Mathematics and Theoretical Computer Science research group at the Faculty of Mathematics and Physics, University of Ljubljana, Slovenia
    • September 2019: Autumn School ‘Proof and Computation’ at Herrsching, Germany
    • September 2018: Autumn School ‘Proof and Computation’ at Fischbachau, Germany
    • November 2017 – December 2017: visited Prof. Norbert Mueller and University of Trier, Trier, Germany
    • October 2017 – November 2017: visited Prof. Alex Simpson and Foundations of Mathematics and Theoretical Computer Science research group at the Faculty of Mathematics and Physics, University of Ljubljana, Slovenia
  • Other activities:
    • KLD2021 / January 2021 / Online / the first Korea Logic Day 2021 / Organizing comittee member
    • WAAC2019 / October 2018 / Daejeon, Korea / The 22nd Japan-Korea Joint Workshop on Algorithms and Computation / Organizing committee member
    • CCA2017 / July 2017 / Daejeon, Korea / Computability and Complexity in Analysis 2017 / Organizing committee member

  • Blog posts:

    • rewriting is induction 05/01/2019

    • Questions in Multivaluedness 08/05/2018

    • Proof as Object 0 07/11/2018

    • Welcome to my blog 05/30/2018

  • Programming Projects:
    • iRRAMx
    • iRRAM-Random
    • irram.sh
    • erlc-js
  • Visit also:
    • Junhee Cho
    • Junguk Lee
    • Donghyun Lim
    • Holger Thies
    • Martin Ziegler
    • And many more!

Sewon's Blog

  • Sewon's Blog
  • swelite@kaist.ac.kr
  • park-sewon

Do you know Heung-min Son?