====== Sewon Park (박세원) ====== //English　｜　[[/jp/sewon_park|日本語]]// DBLP [[https://dblp.org/pid/185/0952-1.html|{{wiki:dblp.png?0x16}}]]　・　GitHub [[https://github.com/park-sewon|{{wiki:github-mark.png?0x16}}]]　・　Google Scholar [[https://scholar.google.co.kr/citations?user=7Yj_Ax4AAAAJ&hl=en|{{https://upload.wikimedia.org/wikipedia/commons/thumb/c/c7/Google_Scholar_logo.svg/2048px-Google_Scholar_logo.svg.png?0x16}}]]　・　LinkedIn [[www.linkedin.com/in/sewon-park-83a446205|{{https://upload.wikimedia.org/wikipedia/commons/thumb/8/81/LinkedIn_icon.svg/1200px-LinkedIn_icon.svg.png?0x16}}]]　・　ORCID [[https://orcid.org/0000-0002-6443-2617 |{{https://info.orcid.org/wp-content/uploads/2019/11/orcid_16x16.png?0x16}}]]　・　Research Map [[https://researchmap.jp/sewonpark|{{wiki:rmap.png?0x16}}]] * //none of the above profiles is being actively maintained. Only this webpage is ☺︎ // 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]]. My research interests include computable analysis, verified exact real-number computation, and formalization of constructive, computable, and classical mathematics in a dependent type theory and its implementation, such as the Coq proof assistant. This webpage works as my CV when it is printed out. Including boxes like this, unnecessary stuff will disappear in printing. I started to post some notes in [[notes|Notes]]. Take a look! ===== Employment ===== * **Postdoctoral Researcher** * Graduate School of Informatics, Kyoto University, Japan (hosted by //Prof. Atsushi Igarashi//) * 1 April 2024 -- current * **Postdoctoral Researcher** * Research Institute for Mathematical Sciences, Kyoto University, Japan (hosted by //[[https://www.kurims.kyoto-u.ac.jp/~kawamura/index_e.html|Prof. Akitoshi Kawamura]]//) * 16 October 2021 -- 31 March 2024 (//1 April 2022 -- 31 March 2024 was supported by JSPS Postdoctoral Fellowship//) ===== Education ===== * **PhD** at [[https://kaist.edu|KAIST]] [[https://cs.kaist.ac.kr|School of Computing]] (Daejeon, South Korea) in Computer Science * Dissertation: [[thesis| Continuous Abstract Data Types for Verified Computation]] (supervised by //Prof. Martin Ziegler//) * 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.** at KAIST School of Computing in Computer Science * Thesis: Verified Real Computation (supervised by //Prof. Martin Ziegler//) * 31 August 2015 -- 18 August 2017 * **B.S.** at KAIST in Physics (main major) and Industrial System Engineering (double major) * 7 February 2011 -- 14 August 2015 ===== Publications ===== //The authors in all my contributions except one marked with ⭐︎ are listed in the alphabetical order// ==== Journals ==== * **Extracting efficient exact real number computation from proofs in constructive type theory** (2024) * //Michal Konečný, Sewon Park, and Holger Thies// * Oxford University Press -- Journal of Logic and Computation (**JLC**), //published online in advance in October 2024// * [[https://doi.org/10.1093/logcom/exae066]] * Preprint available at https://arxiv.org/abs/2202.00891 * ⭐︎**Semantics, Specification Logic, and Hoare Logic of Exact Real Computation** (2024) * //Sewon Park, Franz Brauße, Pieter Collins, SunYoung Kim, Michal Konečný, Gyesik Lee, Norbert Müller, Eike Neumann, Norbert Preining, and Martin Ziegler// * Logical Methods in Computer Science (**LMCS**), June 24, 2024, Volume 20, Issue 2 * [[https://doi.org/10.46298/lmcs-20(2:17)2024|https://doi.org/10.46298/lmcs-20(2:17)2024]] ==== Manuscript ==== * ** Formalizing Hyperspaces and Operations on Subsets of Polish spaces over Abstract Exact Real Numbers** (2024; **submitted**) * //Michal Konečný, Sewon Park, and Holger Thies// * Preprint available at: https://arxiv.org/abs/2410.13508 * **An Imperative Language for Verified Exact Real-Number Computation** (2024; **submitted**) * //Andrej Bauer, Sewon Park, and Alex Simpson// * Preprint available at: https://arxiv.org/abs/2409.11946 ==== Refereed International Conference Publications ==== * **A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations** (2024) * //Sewon Park and Holger Thies// * In: Bertot, Y. and Kutsia, T. and Norrish, M. (eds) 15th International Conference on Interactive Theorem Proving. [[https://www.viam.science.tsu.ge/itp2024/ | ITP 2024]] * Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik * https://doi.org/10.4230/LIPIcs.ITP.2024.30 * **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 ==== 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]] * 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** * 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** * 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 ===== Software ===== * **CAern: Axiomatic Reals and Certified Efficient Exact Real Computation** (//Coq Proof Assistant//) * Michal Konečný, Sewon Park and Holger Thies, * https://github.com/holgerthies/coq-aern * **Coq-clerical: Clerical Coq Formalization** (//Coq Proof Assistant//) * Andrej Bauer and Sewon Park * https://github.com/park-sewon/coq-clerical * **Clerical: Command-like expressions for infinite-precision calculations** (//OCaml//) * Andrej Bauer and Sewon Park * https://github.com/andrejbauer/clerical * **iRRAMx: an extension of iRRAM** (//C++//) * Jiman Hwang, Jihoon Hyun, Hyunwoo Lee, Donghyun Lim, Sewon Park, Holger Thies and Martin Ziegler * https://github.com/realcomputation/iRRAMx * **iRRAM-Random** (//C++//) * Sewon Park * https://github.com/park-sewon/iRRAM-Random ===== Other Activities ===== * ** 2024 Continuity, Computability, Constructivity - From Logic to Algorithms** [[https://www.lix.polytechnique.fr/CCC2024/i.php?Main.Home | CCC2024]] * //Programme Committee member// * October 2-4, 2024, Nice, France * **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 ---- ===== 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]]