朴世原(パク・セウォン|PARK Sewon)
研究分野
職歴
-
特定研究員
-
京都大学大学院情報学研究科(
指導教員:
五十嵐 淳)
-
-
2024年04月01日〜現在
-
JSPS外国人特別研究員
-
特定研究員
-
京都大学 数理解析研究所(指導教員:河村 彰星)
-
-
2021年10月16日〜2022年03月31日
学歴
-
韓国科学技術院(KAIST)
-
博士号(コンピュータサイエンス)
-
-
-
博士論文:
Continuous Abstract Data Types for Verified Computation
-
2017年08月28日〜2021年08月20日
-
修士号(コンピュータサイエンス)
-
学士号 (物理学(主専攻)、産業及びシステム工学(複数専攻))
論文
*星印⭐︎で表示された博士号に関連する論文以外の論文は、すべて著者がアルファベット順に表記されています。
学術雑誌(査読有り)
-
⭐︎
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, June 24, 2024, Volume 20, Issue 2
-
-
Extracting efficient exact real number computation from proofs in constructive type theory (2022,
submitted accepted for publication)
論文原稿(審査中)
-
An Imperative Language for Verified Exact Real-Number Computation (2024;
submitted)
国際学会誌(査読有り)
-
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
-
-
Verified Exact Real Computation with Nondeterministic Functions and Limits (2023)
-
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
-
-
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.
-
-
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
-
-
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
-
プレプリント
-
Randomized Computation of Continuous Data: Is Brownian Motion Computable? (2019)
-
Fouché, Willem, Hyunwoo Lee, Donghyun Lim, Sewon Park, Matthias Schröder, and Martin Ziegler
-
-
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
-
国内学会誌(査読有り)
もっと見る(〜2020年)
-
Compact Subsets in Exact Real Computation (2020)
-
Topological Aspects on Nondetermistic Computation (2020)
-
Grassmannian as Continuous Data Type with Computable Semantics (2019)
-
Seokbin Lee, Donghyun Lim, Sewon Park, Martin Ziegler
-
한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), pp. 1767-1769
-
-
Tensor Calculus in Exact Real Computation on Simplicial Complexes (2018)
-
Chansu Park, Sewon Park, Martin Ziegler
-
한국정보과학회 학술발표논문집 (KIISE Conference Proceedings), pp. 1729-1731
-
学会発表
招待発表
-
Abstract data type for exact real numbers and verified computation Slides
-
Verified computation over real numbers and other continuous objects
-
Toward verified real computation
口頭発表
-
Verifying iRRAM-like implementation of exact real computation
-
Verified Exact Real Computation with Nondeterministic Functions and Limits
-
Towards verified implementation of iterative and interactive real-RAM
もっと見る(〜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
-
Topological Aspects on Nondetermistic Computation
-
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
-
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
-
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
研究訪問
-
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
-
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
-
Autumn School Proof and Computation PC18
-
University of Trier
-
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)
-
Coq-clerical: Clerical Coq Formalization (
Coq Proof Assistant)
-
Clerical: Command-like expressions for infinite-precision calculations (
OCaml)
-
iRRAMx: an extension of iRRAM (
C++)
-
Jiman Hwang, Jihoon Hyun, Hyunwoo Lee, Donghyun Lim, Sewon Park, Holger Thies and Martin Ziegler
-
-
その他
-
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
-
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
-
The first Korea Logic Day 2021 KLD2021
-
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
jp/sewon_park.txt · Last modified: 2024/09/24 11:53 by sewon