====== 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. Please consider subscribing to [[https://groups.google.com/g/korea-logic-ml/about | the Korea Logic Mailing List]] to stay informed about various logic-related events in Korea! 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 ===== * **Computability and Complexity in Analysis 2025** [[http://cca-net.de/cca2025/ | CCA2025]] * //Organizing Committee member // * September 23-26 (to be confirmed), 2025, Kyoto, Japan * **The Fourth Korea Logic Day 2025** [[https://korealogicday.org/2025 | KLD2025]] * //Organizing Committee member // * January 13-15, 2025, Changwon, Korea * ** 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]]