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
- Computability and Complexity in Analysis
- Validated Numerics
- Algorithms for Exact Real Arithmetic
- Ordinary Differential Equations
- Formal proofs and proof assistants
Publications
See also DBLP
- Florian Steinberg, Laurent Thery, Holger Thies: Computable analysis and notions of continuity in Coq. (2020), Accepted for publication in LMCS.
- 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), to appear.
- 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.
- 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.
- 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.
- 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.
- 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
- Michal Konečný, Florian Steinberg, Holger Thies: Continuous and monotone machines.
Theses
- 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)
- Holger Thies: Case Studies in Exact Real Arithmetic -- Implementations and empirical Evaluation. Master thesis, Department of Mathematics, Darmstadt University of Technology (2015)
- 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 Tokyo04/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)
Computability, Continuity, Constructivity - from Logic to Algorithms 2019
Talk: Analytic ordinary differential equations - from computational complexity to efficient and verified algorithms (Invited talk)
Sixteenth International Conference on Computability and Complexity in Analysis
Talk: Formal proofs about metric spaces and continuity in Coq
Research Grants
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/2024
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
Recent Activities
- Programme Committee member for Continuity, Computability, Constructivity (CCC 2020)
- Programme Committee member for Computability and Complexity in Analysis (CCA 2020)
- External Reviewer for the French National Research Agency (ANR), France
- Reviewer for Computability
- Subreviewer for COCOA 2019
Software etc.
Analytic Functions and Ordinary Differential Equations in iRRAM
An extension of the iRRAM C++ framework by general data-types for analytic functions and for solving initial value problems for ordinary differential equations with analytic right-hand side
Links
Junhee Cho / Akitoshi Kawamura / Norbert Müller / Sewon Park / Florian Steinberg / Martin ZieglerLaboratory 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