所属：京都大学大学院情報学研究科　コンピュータソフトウェア分野　特定研究員

メール： Sewon@sewonpark.com　・　 sewon@fos.kuis.kyoto-u.ac.jp

主な研究分野：計算可能解析学、検証付き精密実数計算、型理論で古典的・構成主義的・計算的な数学を定型化する事、そしてその定型化をCOQ等の証明支援系で実現する事等

• 特定研究員

  • 京都大学大学院情報学研究科（指導教員：五十嵐 淳）
  • 形式検証とシステムソフトウェアの協働によるゼロトラストIoT
  • 2024年04月01日〜現在
• JSPS外国人特別研究員

  • 京都大学 数理解析研究所（指導教員：河村 彰星）
  • 連続系における高階函数の保証つき厳密計算
  • 2022年04月01日〜2024年03月31日
• 特定研究員

  • 京都大学 数理解析研究所（指導教員：河村 彰星）
  • 連続系の複雑さを解明する計算理論
  • 2021年10月16日〜2022年03月31日

• 韓国科学技術院（KAIST）

  • 博士号（コンピュータサイエンス）

    • 計算量及び実数計算研究室（電算学部）
    • 指導教員：Prof. Martin Ziegler
    • 博士論文： Continuous Abstract Data Types for Verified Computation

      • 要約： The Bulletin of Symbolic Logic, 27(4), 531-531. doi:10.1017/bsl.2021.51
    • 2017年08月28日〜2021年08月20日
  • 修士号（コンピュータサイエンス）

    • 計算量及び実数計算研究室（電算学部）
    • 指導教員：Prof. Martin Ziegler
    • 修士論文：Verified Real Computation
    • 2015年08月31日〜2017年08月18日
  • 学士号 （物理学（主専攻）、産業及びシステム工学（複数専攻））

    • 2011年02月07日〜2015年08月14日

＊星印⭐︎で表示された博士号に関連する論文以外の論文は、すべて著者がアルファベット順に表記されています。

• 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

• 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

• 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. 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 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. 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. 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. 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. WALCOM 2018
  • Lecture Notes in Computer Science, vol 10755. Springer, Cham
  • https://doi.org/10.1007/978-3-319-75172-6_12

• 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

もっと見る（〜2020年）

• Abstract data type for exact real numbers and verified computation Slides

  • Invited talk
  • Sewon Park
  • The 17th International Conference on Computability, Complexity and Randomness 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 Link
  • Mar 02 – 04, 2022, Akita, Japan
• Toward verified real computation

  • Invited talk
  • Sewon Park
  • Continuity, Computability, Constructivity From Logic to Algorithms CCC 2021
  • Sep 20 – 24, 2021, Online

• Verifying iRRAM-like implementation of exact real computation

  • Sewon Park, Holger Thies
  • Continuity, Computability, Constructivity - From Logic to Algorithms 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 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 CCA 2023
  • Sep 07 – 09, 2023, Dubrovnik, Croatia

もっと見る（〜2022年）

• Korean Mathematical Society 2024 Spring meeting and KAIST

  • April 17 – 21, 2024, Daejeon Convention Center and KAIST, Daejeon, Korea
• 数学基礎論サマースクール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 PC19

  • September 2019, Herrsching, Germany
• Autumn School Proof and Computation 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

• 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

• 2024 Continuity, Computability, Constructivity - From Logic to Algorithms CCC2024

  • Programme Committee member
  • October 2-4, 2024, Nice, France
• The third Korea Logic Day 2024 KLD2024

  • Organizing Committee member
  • 12 January 2024, online
• 2023 Continuity, Computability, Constructivity - From Logic to Algorithms CCC2023

  • Programme Committee and Organizing Committee member
  • September 25 - 29, 2023, Kyoto, Japan
• The second Korea Logic Day 2022 KLD2022

  • Organizing Committee member
  • 14 January 2022, online
• The first Korea Logic Day 2021 KLD2021

  • Organizing Committee member
  • 14 January 2021, online
• The 22nd Japan-Korea Joint Workshop on Algorithms and Computation WAAC2019

  • Organizing Committee member
  • October 4-5, 2019, Daejeon, Korea
• Computability and Complexity in Analysis 2017 CCA2017

  • Organizing Committee member
  • July 24-27, 2017, Daejeon, Korea