Holger Thies

Associate Professor · Mathematical Informatics Group · Kyoto University

Holger Thies

I am an Associate Professor 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, and formal proofs and proof assistants.

Travel All travel →

  • Nov 16–17, 2026
    TPP 2026 · Tokyo, Japan

Recent

Recent publications All publications →

  1. Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
    Holger Thies
    In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2026), 2026
  2. Computable Analysis for Extraction of Certified Programs and Its Applications
    Holger Thies
    In Crossroads of Computability and Logic: 21st Conference on Computability in Europe (CiE 2025), 2025
  3. Extracting efficient exact real number computation from proofs in constructive type theory
    Michal Konečný, Sewon Park, and Holger Thies
    Journal of Logic and Computation, 2025
  4. A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations
    Sewon Park and Holger Thies
    In 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024
  5. Formalizing Hyperspaces for Extracting Efficient Exact Real Computation
    Michal Konečný, Sewon Park, and Holger Thies
    In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), 2023

Recent talks All talks →