English | 日本語

Holger Thies

I am a (Program-Specific) Lecturer in the Mathematical Informatics Group at the Graduate School of Human and Environmental Science, Kyoto University.

Research Interests

Travel plans

November 25-26, TPP 2024, Fukuoka, Japan
Past
Holger Thies

researchmap


thies.holger.5c@kyoto-u.ac.jp
Data Protection Declaration

Publications

See also DBLP

  1. Michal Konečný, Sewon Park, Holger Thies: Extracting efficient exact real number computation from proofs in constructive type theory. Journal of Logic and Computation (2024), exae066.
  2. Sewon Park, Holger Thies: A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations. Proc. of the 15th International Conference on Interactive Theorem Proving (ITP2024) (2024), 30:1-30:19.
  3. Michal Konečný, Sewon Park, Holger Thies: Formalizing Hyperspaces for Extracting Efficient Exact Real Computation. Proc. of the 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) (2023), 59:1--59:16.
  4. Michal Konečný, Sewon Park, Holger Thies: Certified Computation of Nondeterministic Limits. NASA Formal Methods Symposium 2022 (2022), pp. 771-789.
  5. Svetlana Selivanova, Florian Steinberg, Holger Thies, Martin Ziegler: Exact Real Computation of Solution Operators for Linear Analytic Systems of Partial Differential Equations. Proc. of the 23rd International Workshop on Computer Algebra in Scientific Computing (CASC 2021) (2021), pp. 370-390.
  6. Michal Konečný, Sewon Park, Holger Thies: Axiomatic Reals and Certified Efficient Exact Real Computation. Proc. of the 27th International Workshop on Logic, Language, Information, and Computation (Wollic 2021) (2021), pp. 252-268.
  7. Florian Steinberg, Laurent Thery, Holger Thies: Computable analysis and notions of continuity in Coq. Logical Methods of Computer Science, Vol. 17(2) (2021), .
  8. Michal Konečný, Florian Steinberg, Holger Thies: Computable Analysis for Verified Exact Real Computation. Proc. of the 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020), December 14-18, 2020. (2020), 50:1-50:18.
  9. Michal Konečný, Florian Steinberg, Holger Thies: Continuous and Monotone Machines. Proc. of the 45rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2020), August 24-28, 2020. (2020), pp. 56:1-56:16.
  10. Florian Steinberg, Laurent Thery, Holger Thies: Quantitative Continuity and Computable Analysis in Coq. Proc. of the 10th International Conference on Interactive Theorem Proving (ITP 2019), September 9-12, 2019, Portland, OR, USA (2019), pp. 28:1-28:21.
  11. Akitoshi Kawamura, Florian Steinberg, Holger Thies: Second-order linear-time computability with applications to computable analysis. Proc. of the 15th Annual Conference on Theory and Applications of Models of Computation (TAMC 2019), April 13-16, 2019, Kitakyushu, Japan (2019), Chapter 21.
  12. Akitoshi Kawamura, Holger Thies, Martin Ziegler: Average-case polynomial-time computability of Hamiltonian dynamics. Proc. of the 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018), August 27-31, 2018, Liverpool, UK. (2018), pp. 30:1-30:17.
  13. Akitoshi Kawamura, Florian Steinberg, Holger Thies: Parameterized Complexity for Uniform Operators on Multidimensional Analytic Functions and ODE Solving. Proc. of the 25th International Workshop on Logic, Language, Information, and Computation (WoLLIC 2018), July 24-27, 2018, Bogota, Colombia (2018), pp. 223-236.

Preprints

  1. Michal Konečný, Sewon Park, Holger Thies: Formalizing Hyperspaces and Operations on Subsets of Polish spaces over Abstract Exact Real Numbers.
  2. Michal Konečný, Florian Steinberg, Holger Thies: Continuous and monotone machines.

Theses

  1. Holger Thies: Uniform computational complexity of ordinary differential equations with applications to dynamical systems and exact real arithmetic. PhD thesis, Graduate School of Arts and Sciences, University of Tokyo (2018)
  2. Holger Thies: Case Studies in Exact Real Arithmetic -- Implementations and empirical Evaluation. Master thesis, Department of Mathematics, Darmstadt University of Technology (2015)
  3. Holger Thies: Complexity Theory and Practice of Integrating Lipschitz-continuous functions in Exact Real Arithmetic (in German). Bachelor thesis, Department of Mathematics, Darmstadt University of Technology (2011)

Employment

Program-Specific Lecturer
Kyoto University, Graduate School of Human and Environmental Science
04/2021 -
Assistant Professor
Kyushu University, Department of Informatics
Mathematical Engineering Lab
05/2019 - 04/2021
JSPS Research Fellow (PD)
Kyushu University
09/2018 - 05/2019
JSPS Research Fellow (DC2)
University of Tokyo
04/2018 - 08/2018
Researcher (part-time)
Darmstadt University of Technology
04/2015 - 08/2015

Education

University of Tokyo
Ph.D., Graduate School of Arts and Science, Computing Systems Research Group
09/2015 - 08/2018
Darmstadt University of Technology
MSc., Mathematics with Computer Science
04/2013 - 04/2015
Darmstadt University of Technology
BSc., Mathematics
10/2009 - 04/2013
Darmstadt University of Technology
BSc., Computer Science
10/2008 - 10/2011

Long-term research stays etc.

For short-term stays see Travel page

University of Tokyo
Exchange Research Student, Graduate School of Information Science and Technology
10/2013 - 03/2014
University of Oslo
Exchange Student, Department of Mathematics
08/2011 - 06/2012

Selected Conference Talks (Show All)

Autumn school Proof and Computation

Talk: Extracting efficient programs from proofs in analysis

September 2024
Fischbachau, Germany
PC24

17th International Conference on Computability, Complexity and Randomness

Talk: Applications of Exact Real Computation in Particle Physics

March 2024
Nagoya, Japan
CCR 2024

Fifth Workshop on Digitalization and Computable Models

Talk: Formal verification and program extraction for efficient computations over real numbers and hyperspaces (Invited Talk)

October 2023
Astana, Kazakhstan (Online)
WDCM 2023

Continuity, Computability, Constructivity - From Logic to Algorithms 2023

Talk: Advances in verified set and function calculi in Coq

September 2023
Kyoto, Japan
CCC 2023

Autumn school Proof and Computation

Talk: Complexity Theory in Analysis with Applications to Differential Equations (Invited Talk)

September 2021
Online
PCV21

Computability, Continuity, Constructivity - from Logic to Algorithms 2019

Talk: Analytic ordinary differential equations - from computational complexity to efficient and verified algorithms (Invited talk)

September 2019
Ljubljana, Slovenia
CCC2019

Sixteenth International Conference on Computability and Complexity in Analysis

Talk: Formal proofs about metric spaces and continuity in Coq

July 2019
Zagreb, Croatia
CCA2019

Research Grants

Kakenhi Grant-in-Aid for Early-Career Scientists
Research on Computable Analysis and Verification of Efficient Exact Real Computation, Grant number 24K20735 (Principal Investigator)
04/2024 - 03/2029
Kakenhi Grant-in-Aid for Scientific Research (B)
連続な空間上の計算とその複雑さの研究 , Grant number 23K28036 (Co-Investigator, Princial Investigator: Hideki Tsuiki)
04/2023 - 03/2028
Kakenhi Grant-in-Aid for Early-Career Scientists
Computational complexity and practice of verified and efficient algorithms for dynamical systems, Grant number 20K19744 (Principal Investigator)
04/2020 - 03/2025
Kakenhi Grant-in-Aid for JSPS Fellows
Towards efficient solvers for ordinary differential equations in exact real arithmetic, Grant number 18J10407 (Principal Investigator)
04/2018 - 03/2020


Links

Junhee Cho / Akitoshi Kawamura / Norbert Müller / Sewon Park / Florian Steinberg / Martin Ziegler
Laboratory for Data Science Frontier Research / Circuits, Systems, and Communication Networks Laboratory / Computing System Research Group, University of Tokyo / Logic Group, TU Darmstadt / Imai Lab, University of Tokyo / Ishihara Lab, JAIST / Complexity and Real Computation Lab, KAIST