User Tools

Site Tools


sewon_park

Sewon Park (박세원)

English | 日本語

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

* none of the above profiles is being actively maintained. Only this webpage is ☺︎

I am a postdoctoral researcher hosted by Prof. Atsushi Igarashi at the Computer Software Group, Kyoto University. You may contact me by Sewon@sewonpark.com or by 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 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. 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 Prof. Akitoshi Kawamura)
    • 16 October 2021 – 31 March 2024 (1 April 2022 – 31 March 2024 was supported by JSPS Postdoctoral Fellowship)

Education

  • PhD at KAIST School of Computing (Daejeon, South Korea) in Computer Science
  • 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)
  • ⭐︎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

Manuscript

  • Formalizing Hyperspaces and Operations on Subsets of Polish spaces over Abstract Exact Real Numbers (2024; submitted)
  • An Imperative Language for Verified Exact Real-Number Computation (2024; submitted)

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. 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)
  • Axiomatic Reals and Certified Efficient Exact Real Computation (2021)
  • Computing Periods … (2018)

Preprints

  • Randomized Computation of Continuous Data: Is Brownian Motion Computable? (2019)
  • Computable Operations on Compact Subsets of Metric Spaces with Applications to Fr\’echet Distance and Shape Optimization (2017)

Short Peer-reviewed Conference Proceedings

Show more (-2020)

Conference Talks

These are lists automatically generated from my .bib database. (To be precise, it automatically generates the lists in 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 Slides
    • 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
    • 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
    • Continuity, Computability, Constructivity From Logic to Algorithms 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 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

Show more (-2022)

Research Visits

  • 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

Software

Other Activities

  • Computability and Complexity in Analysis 2025 CCA2025
    • Organizing Committee member
    • September 23-26 (to be confirmed), 2025, Kyoto, Japan
  • The Fourth Korea Logic Day 2025 KLD2025
    • Organizing Committee member
    • January 13-15, 2025, Changwon, Korea
  • 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

sewon_park.txt · Last modified: 2025/01/16 11:13 by sewon