ホーム | Holger Thies

研究分野：計算可能解析学、計算理論、精度保証付き数値計算、計算機援用証明

出張出張記録 →

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

2026年6月

Extracting certified programs from type-theoretic proofs in analysis and topology

Logic Colloquium 2026, Swansea, UK
2026年4月

Spaces of Sequences in Computable Analysis and Applications to Differential Equations

Differentiation in category theory and program semantics, Kyoto, Japan
2025年12月

Verified Computation of ODE Trajectories in Rocq

The 21st Theorem Proving and Provers Meeting, Sendai, Japan
2025年9月

A Verified Power-Series Method for Multivariate IVPs

Twenty-Second International Conference on Computability and Complexity in Analysis, Kyoto, Japan
2025年7月

Computable Analysis for Extraction of Certified Programs and its Applications（招待講演）

Computability in Europe 2025, Lisbon, Portugal