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 homepage 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.

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

  • 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: 2024/11/01 12:11 by sewon