====== Sewon Park ======
I am a postdoctoral researcher hosted by [[https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/index.html.en | Prof. Atsushi Igarashi]] at the [[https://www.fos.kuis.kyoto-u.ac.jp|Computer Software Group]], Kyoto University. You may contact me by [[Sewon@sewonpark.com | Sewon@sewonpark.com]] or by [[sewon@fos.kuis.kyoto-u.ac.jp| sewon@fos.kuis.kyoto-u.ac.jp]].
This webpage works as my CV when it is printed out.
Including boxes like this, unnecessary stuff will disappear in printing.
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.
===== Research Interests =====
* [[http://cca-net.de | Computability and complexity in analysis ]]
* [[https://github.com/holgerthies/coq-aern | Certified / Verified exact real number computation]]
* [[https://users.ece.cmu.edu/~koopman/des_s99/formal_methods/ | Formal methods]]
* [[https://www.cambridge.org/core/books/theories-of-programming-languages/19530A88F3471B2A7D9891770B21DAF9 | Programming language theory]]
* [[https://philpapers.org/rec/BRIVOC | Constructive mathematics]]
* [[http://www.cs.cmu.edu/afs/cs/Web/People/andrej/thesis/ | Type theories and their interpretations]]
===== Employment =====
* **Postdoctoral Researcher**
* Graduate School of Informatics, Kyoto University, Japan
* 1 April 2024 -- current
* **Postdoctoral Researcher**
* Research Institute for Mathematical Sciences, Kyoto University, Japan
* 16 October 2021 -- 31 March 2024
* //1 April 2022 -- 31 March 2024 was supported by JSPS Postdoctoral Fellowship for Research in Japan (Standard) on "Verified Exact Computation over Continuous Higher Types"//
===== Education =====
* **KAIST, Daejeon, Korea**
* **PhD.** in Computer Science
* Complexity and Real Computation Laboratory, School of Computing
* dissertation: [[thesis| 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 major)
* 7 February 2011 -- 14 August 2015
===== Publications =====
See also [[https://dblp.org/pers/hd/p/Park_0001:Sewon | DBLP]]
The authors in all my contributions are written in the alphabetical order
==== Journals ====
* **"Extracting efficient exact real number computation from proofs in constructive type theory"** (2022, submitted accepted for publication at a journal)
* //Michal Konečný, Sewon Park, and Holger Thies//
* Preprint at https://arxiv.org/abs/2202.00891
==== Refereed Conference Publications ====
* **"Verified Exact Real Computation with Nondeterministic Functions and Limits"** (2023)
* //Sewon Park//
* In: Fernau, H., Jansen, K. (eds) Fundamentals of Computation Theory [[https://www.uni-trier.de/en/universitaet/fachbereiche-faecher/fachbereich-iv/faecher/informatikwissenschaften/professuren/theoretische-informatik/research/conferences-and-workshops/fct-2023 | FCT 2023]]
* Lecture Notes in Computer Science, vol 14292. Springer, Cham.
* https://doi.org/10.1007/978-3-031-43587-4_26
* **"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. [[https://mfcs2023.labri.fr | MFCS 2023]]
* Leibniz International Proceedings in Informatics (LIPIcs), vol 272. Schloss Dagstuhl -- Leibniz-Zentrum für Informatik
* https://doi.org/10.4230/LIPIcs.MFCS.2023.59
* **"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. [[https://nfm2022.caltech.edu | 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. [[https://wollic.org/wollic2021/ | WoLLIC 2021]]
* Lecture Notes in Computer Science, vol 13038. Springer, Cham
* https://doi.org/10.1007/978-3-030-88853-4_16
* **“Computing Periods …”** (2018)
* //Junhee Cho, Sewon Park, and Martin Ziegler //
* In: Rahman M., Sung WK., Uehara R. (eds) WALCOM: Algorithms and Computation. [[https://cse.buet.ac.bd/walcom2018/ | WALCOM 2018]]
* Lecture Notes in Computer Science, vol 10755. Springer, Cham
* https://doi.org/10.1007/978-3-319-75172-6_12
==== 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//
* 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
==== Short Peer-reviewed Conference Proceedings ====
++++ Show more (-2020)|
* **“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
++++
===== Conference Talks =====
These are lists automatically generated from my [[https://sewonpark.com/bib?do=export_text | .bib database]].
(To be precise, it automatically generates the lists in [[https://sewonpark.com/workspace/bib | 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** [[https://drive.google.com/file/d/1vxT4D7JlMQTsPX8zOGmyz8CdJNFM67Ds/view?usp=share_link|Slides]]
* //Invited talk//
* Sewon Park
* The 17th International Conference on Computability, Complexity and Randomness [[https://sites.google.com/view/ccr2024/home|CCR2024]]
* March 11-15, 2024, Nagoya, Japan
* **Verified computation over real numbers and other continuous objects**
* //Tutorial talk//
* Sewon Park
* The second Japan-Russia workshop on effective descriptive set theory, computable analysis and automata [[https://sites.google.com/view/jp-ru-logic2022/ | Link]]
* Mar 02 -- 04, 2022, Akita, Japan
* **Toward verified real computation**
* //Invited talk//
* Sewon Park
* Continuity, Computability, Constructivity From Logic to Algorithms [[https://www.cs.bham.ac.uk/~axj/ccc2021/index.html#programme | CCC 2021]]
* Sep 20 -- 24, 2021, Online
==== Contributed Talks ====
* **Verifying iRRAM-like implementation of exact real computation**
* Sewon Park, Holger Thies
* Continuity, Computability, Constructivity - From Logic to Algorithms [[https://www.i.h.kyoto-u.ac.jp/ccc2023/ | CCC 2023]]
* Sep 25 -- 29, 2023, Kyoto, Japan
* **Verified Exact Real Computation with Nondeterministic Functions and Limits**
* Sewon Park
* 24th International Symposium on Fundamentals of Computation Theory [[https://www.uni-trier.de/en/universitaet/fachbereiche-faecher/fachbereich-iv/faecher/informatikwissenschaften/professuren/theoretische-informatik/research/conferences-and-workshops/fct-2023 | FCT 2023]]
* Sep 18 -- 21, 2023, Trier, Germany (online talk)
* **Towards verified implementation of iterative and interactive real-RAM**
* Sewon Park, Holger Thies
* Twentieth International Conference on Computability and Complexity in Analysis [[http://cca-net.de/cca2023/ | CCA 2023]]
* Sep 07 -- 09, 2023, Dubrovnik, Croatia
++++ 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 [[https://www.kms.or.kr/conference/2022_fall | 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 [[https://events.math.unipd.it/ccc2022/#venue | 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 [[http://cca-net.de/cca2022/ | 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 [[http://aaac2021.ie.nthu.edu.tw/ | 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 [[https://www.kms.or.kr/meetings/fall2021/ | KMS Fall 2021]]
* Oct 20 -- 22, 2021, Online
* **Intuitionistic Logic, Type Theory, and Computer Science**
* Sewon Park
* the first Korea Logic Day 2021 [[https://korealogicday.org/2021 | KLD 2021]]
* Jan 14 -- 14, 2021, Online
* **Topological Aspects on Nondetermistic Computation**
* Donghyun Lim, Sewon Park
* Korea Software Congress 2020 [[http://ksc2020.kiise.or.kr/wp/Home.asp/ | KSC 2020]]
* Dec 21 -- 23, 2020, Online
* **Clerical: an Imperative Language for Verified Real-number Computation**
* Andrej Bauer, Sewon Park, Alex Simpson
* Seventeenth International Conference on Computability and Complexity in Analysis [[http://cca-net.de/cca2020/ | 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 [[http://www.kms.or.kr/meetings/spring2020/ | KMS Spring 2020]]
* Jul 03 -- 03, 2020, Online
* **Axiomatic Reals in Type Theory for Program Extraction**
* Sewon Park
* Computability, Continuity, Constructivity - from Logic to Algorithms [[https://www.fmf.uni-lj.si/~simpson/ccc2019/ | CCC 2019]]
* Sep 2019, Ljubljana, Slovenia
* **Interval Gaussian Algorithm for Singular Interval Matrices**
* Sewon Park
* Fall Workshop on Algorithms and Computation [[http://tcs.postech.ac.kr/workshops/fwac18/ | 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 [[http://scan2018.oishi.info.waseda.ac.jp/ | SCAN 2018]]
* Sep 2018, Tokyo, Japan
* **Reliable Diagonalization of Degenerate Matrices**
* Sewon Park, Martin Ziegler
* Computability and Complexity in Analysis 2017 [[http://cca-net.de/cca2017/ | CCA 2017]]
* Jul 2017, Daejeon, Korea
* **Implementation and Empirical Evaluation of two Algorithms for Computing Characteristic Polynomials' Coefficients in Exact Real Arithmetic**
* Sewon Park
* Fall Workshop on Algorithms and Computation [[http://tcs.postech.ac.kr/workshops/fwac16/ | 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 [[http://dopal.cs.uec.ac.jp/waac16/ | WAAC 2016]]
* Aug 2016, Hakodate, Japan
* **On Formal Verification in Imperative Multivalued Programming over Continuous Data Types**
* Norbert Th., Sewon Park, Norbert Preining, Martin Ziegler
* Computability and Complexity in Analysis 2016 [[http://cca-net.de/cca2016/ | CCA 2016]]
* Jun 2016, Faro, Portugal
++++
===== Research Visits =====
* ** Korean Mathematical Society 2024 Spring meeting** and KAIST
* April 17 -- 21, 2024, Daejeon Convention Center and KAIST, Daejeon, Korea
* **数学基礎論サマースクール2023** [[http://kenshi.miyabe.name/kisoron_school_2023/|link]]
* September 11 -- 15, 2023, Meiji University, Tokyo, Japan
* **Laboratoire d'informatique de l'École polytechnique**
* Prof. Olivier Bournez
* September 4 -- 6, 2023, Palaiseau, France
* **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** [[http://www.mathematik.uni-muenchen.de/~schwicht/pc19.php | PC19]]
* September 2019, Herrsching, Germany
* **Autumn School Proof and Computation** [[https://www.mathematik.uni-muenchen.de/~schwicht/pc18.php | 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 and Prof. Andrej Bauer
* October -- November, 2017, Ljubljana, Slovenia
===== Other Activities =====
* **The third Korea Logic Day 2024** [[https://korealogicday.org/2024 | KLD2024]]
* //Organizing Committee member//
* 12 January 2024, online
* ** 2023 Continuity, Computability, Constructivity - From Logic to Algorithms** [[https://www.i.h.kyoto-u.ac.jp/ccc2023/ | CCC2023]]
* //Programme Committee and Organizing Committee member//
* September 25 - 29, 2023, Kyoto, Japan
* **The second Korea Logic Day 2022** [[https://korealogicday.org/2022 | KLD2022]]
* //Organizing Committee member//
* 14 January 2022, online
* **The first Korea Logic Day 2021** [[https://korealogicday.org/2021 | KLD2021]]
* //Organizing Committee member//
* 14 January 2021, online
* **The 22nd Japan-Korea Joint Workshop on Algorithms and Computation** [[https://kaist.theoryofcomputation.asia/waac2019 | WAAC2019]]
* //Organizing Committee member//
* October 4-5, 2019, Daejeon, Korea
* **Computability and Complexity in Analysis 2017** [[http://cca-net.de/cca2017/ | CCA2017]]
* //Organizing Committee member //
* July 24-27, 2017, Daejeon, Korea
===== Software =====
* [[https://github.com/holgerthies/coq-aern | cAERN]]
* [[https://github.com/realcomputation/iRRAMx | iRRAMx]]
* [[https://github.com/park-sewon/iRRAM-Random | iRRAM-Random]]
* [[https://github.com/park-sewon/irram.sh | irram.sh]]
* [[https://park-sewon.github.io/workspace/ | erlc-js]]
===== Links =====
[[http://cid.uni-trier.de/participants/ | CID]]
/
[[https://korealogicday.org/ | Korea Logic Day]]
/
[[https://andrej.com | Andrej Bauer]]
/
[[https://junheecho.com | Junhee Cho]]
/
[[https://www.kurims.kyoto-u.ac.jp/~kawamura/ | Akitoshi Kawamura]]
/
[[https://sites.google.com/site/leejunguk0323/home | Junguk Lee]]
/
[[https://www.donghyunlim.com | Donghyun Lim]]
/
[[https://floriansteinberg.github.io | Florian Steinberg]]
/
[[http://www.holgerthies.com | Holger Thies]]
/
[[https://cj-xu.github.io | Chuangjie Xu]]
/
[[http://ziegler.theoryofcomputation.asia | Martin Ziegler]]