- 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 Jiman Hwang. “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:
- Visit also:
- Junhee Cho
- Junguk Lee
- Donghyun Lim
- Holger Thies
- Martin Ziegler
- And many more!