朴世原（パク・セウォン｜PARK Sewon）

朴世原（パク・セウォン｜PARK Sewon）

English　｜　日本語

DBLP 　・　GitHub 　・　Google Scholar 　・　LinkedIn 　・　ORCID 　・　Research Map

＊ 上記のプロファイルは積極的に管理されていません。私に関する最新の情報はこのホームページを確認してください。 ☺︎

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

メール： 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日

論文

DBLPもご参照ください

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

学術雑誌（査読有り）

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年）

A type-theoretical interpretation of intuitionistic fixed point logic
- Ulrich Berger, Sewon Park, Holger Thies, Hideki Tsuiki
- 2022 Global KMS International Conference 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 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 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 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 KMS Fall 2021
- Oct 20 – 22, 2021, Online
Intuitionistic Logic, Type Theory, and Computer Science
- Sewon Park
- the first Korea Logic Day 2021 KLD 2021
- Jan 14 – 14, 2021, Online
Topological Aspects on Nondetermistic Computation
- Donghyun Lim, Sewon Park
- Korea Software Congress 2020 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 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 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 CCC 2019
- Sep 2019, Ljubljana, Slovenia
Interval Gaussian Algorithm for Singular Interval Matrices
- Sewon Park
- Fall Workshop on Algorithms and Computation 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 SCAN 2018
- Sep 2018, Tokyo, Japan
Reliable Diagonalization of Degenerate Matrices
- Sewon Park, Martin Ziegler
- Computability and Complexity in Analysis 2017 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 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 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 CCA 2016
- Jun 2016, Faro, Portugal

研究訪問

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

リンク

CID　・　 Korea Logic Day　・　 Andrej Bauer　・　 Junhee Cho　・　 Akitoshi Kawamura　・　 Junguk Lee　・　 Donghyun Lim　・　 Florian Steinberg　・　 Holger Thies　・　 Chuangjie Xu　・　 Martin Ziegler

Table of Contents