publications

See also my DBLP page.

Preprints

  1. Formal verification of tilt estimation using the Rocq prover
    Reynald Affeldt, Lynda Bentoucha, Yoshihiro Ishiguro, and Holger Thies
    arXiv:2609.25561, 2026
  2. Algorithmic Cost in “Exact Real Computation”
    Jihoon Hyun, Holger Thies, and Martin Ziegler
    arXiv:2608.23603, 2026
  4. Continuous and Monotone Machines
    Michal Konečný, Florian Steinberg, and Holger Thies
    arXiv:2005.01624, 2020

Journal and conference papers

2026

  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

2025

  1. 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
  2. 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

2024

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

2023

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

2022

  1. Certified Computation of Nondeterministic Limits
    Michal Konečný, Sewon Park, and Holger Thies
    In NASA Formal Methods: 14th International Symposium (NFM 2022), 2022

2021

  1. Exact Real Computation of Solution Operators for Linear Analytic Systems of Partial Differential Equations
    Svetlana Selivanova, Florian Steinberg, Holger Thies, and Martin Ziegler
    In Computer Algebra in Scientific Computing: 23rd International Workshop (CASC 2021), 2021
  2. Axiomatic Reals and Certified Efficient Exact Real Computation
    Michal Konečný, Sewon Park, and Holger Thies
    In Logic, Language, Information, and Computation: 27th International Workshop (WoLLIC 2021), 2021
  3. Computable analysis and notions of continuity in Coq
    Florian Steinberg, Laurent Théry, and Holger Thies
    Logical Methods in Computer Science, 2021

2020

  1. Computable Analysis for Verified Exact Real Computation
    Michal Konečný, Florian Steinberg, and Holger Thies
    In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020), 2020
  2. Continuous and Monotone Machines
    Michal Konečný, Florian Steinberg, and Holger Thies
    In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020), 2020

2019

  1. Quantitative Continuity and Computable Analysis in Coq
    Florian Steinberg, Laurent Théry, and Holger Thies
    In 10th International Conference on Interactive Theorem Proving (ITP 2019), 2019
  2. Second-Order Linear-Time Computability with Applications to Computable Analysis
    Akitoshi Kawamura, Florian Steinberg, and Holger Thies
    In Theory and Applications of Models of Computation: 15th Annual Conference (TAMC 2019), 2019

2018

  1. Average-Case Polynomial-Time Computability of Hamiltonian Dynamics
    Akitoshi Kawamura, Holger Thies, and Martin Ziegler
    In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018), 2018
  2. Parameterized Complexity for Uniform Operators on Multidimensional Analytic Functions and ODE Solving
    Akitoshi Kawamura, Florian Steinberg, and Holger Thies
    In Logic, Language, Information, and Computation: 25th International Workshop (WoLLIC 2018), 2018

Theses

  2. Case Studies in Exact Real Arithmetic – Implementations and Empirical Evaluation
    Holger Thies
    Department of Mathematics, Darmstadt University of Technology, 2015
  3. Complexity Theory and Practice of Integrating Lipschitz-continuous functions in Exact Real Arithmetic (in German)
    Holger Thies
    2011