 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
 KAIST, Daejeon, S. Korea
 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), 17671769. 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), 17291731. 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/9783319751726_12
 Chansu Park, JiWon 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 Realnumber 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 JapanKorea 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 MiniWorkshop / 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 JapanKorea 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:
 Visit also:
 Junhee Cho
 Junguk Lee
 Donghyun Lim
 Holger Thies
 Martin Ziegler
 And many more!