基本情報

学部兼担

• 総合人間学部
• 国際高等教育院
• 国際高等教育院
• 総合人間学部

学位

• 博士（学術）(東京大学)
• 修士（数学）(ダルムシュタット工科大学)

経歴

• 自 2021年04月, 至 現在

  京都大学, 大学院人間・環境学研究科, 特定講師
• 自 2019年05月, 至 2021年04月

  九州大学, システム情報科学研究院, 助教
• 自 2018年09月, 至 2019年04月

  日本学術振興会, 特別研究員 (PD)
• 自 2018年04月, 至 2018年08月

  日本学術振興会, 特別研究員 (DC 2)
• 自 2015年04月, 至 2015年08月

  ダルムシュタット工科大学, Department of Mathematics, Researcher

使用言語

• 日本語
• 英語

ID,URL

• J-Global ID

  201901005618652421

• 外部リンク

  http://www.holgerthies.com

researchmap URL

• https://researchmap.jp/hthies

研究

研究分野

• 情報通信, 情報学基礎論

論文

• Computable Analysis for Extraction of Certified Programs and Its Applications

  Holger Thies

  2025年

  
• A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations.

  Sewon Park 0001; Holger Thies

  ITP, 2024年

  
• Formalizing Hyperspaces for Extracting Efficient Exact Real Computation.

  Michal Konecný; Sewon Park 0001; Holger Thies

  MFCS, 2023年

  
• Extracting efficient exact real number computation from proofs in constructive type theory.

  Michal Konecný; Sewon Park 0001; Holger Thies

  CoRR, 2022年

  
• Certified Computation of Nondeterministic Limits

  Michal Konečný; Sewon Park; Holger Thies

  NASA Formal Methods - 14th International Symposium(NFM), 2022年

  
• Axiomatic Reals and Certified Efficient Exact Real Computation.

  Michal Konecný; Sewon Park 0001; Holger Thies

  Logic, Language, Information, and Computation - 27th International Workshop(WoLLIC), 2021年

  
• Exact Real Computation of Solution Operators for Linear Analytic Systems of Partial Differential Equations.

  Svetlana Selivanova; Florian Steinberg 0001; Holger Thies; Martin Ziegler 0001

  Computer Algebra in Scientific Computing - 23rd International Workshop(CASC), 2021年

  
• Computable analysis and notions of continuity in Coq.

  Florian Steinberg 0001; Laurent Théry; Holger Thies

  Log. Methods Comput. Sci., 2021年

  
• Continuous and monotone machines.

  Michal Konecný; Florian Steinberg 0001; Holger Thies

  CoRR, 2020年

  
• Computable Analysis for Verified Exact Real Computation.

  Michal Konecný; Florian Steinberg 0001; Holger Thies

  40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science(FSTTCS), 2020年

  
• Continuous and Monotone Machines.

  Michal Konecný; Florian Steinberg 0001; Holger Thies

  Leibniz International Proceedings in Informatics, LIPIcs, 2020年

  
• Quantitative continuity and computable analysis in Coq.

  Florian Steinberg 0001; Laurent Théry; Holger Thies

  CoRR, 2019年

  
• Second-Order Linear-Time Computability with Applications to Computable Analysis.

  Akitoshi Kawamura; Florian Steinberg 0001; Holger Thies

  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2019年, 査読有り

  
• Quantitative Continuity and Computable Analysis in Coq.

  Florian Steinberg 0001; Laurent Théry; Holger Thies

  Leibniz International Proceedings in Informatics, LIPIcs, 2019年, 査読有り

  
• Parameterized Complexity for Uniform Operators on Multidimensional Analytic Functions and ODE Solving.

  Akitoshi Kawamura; Florian Steinberg 0001; Holger Thies

  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2018年, 査読有り

  
• Average-Case Polynomial-Time Computability of Hamiltonian Dynamics.

  Akitoshi Kawamura; Holger Thies; Martin Ziegler 0001

  Leibniz International Proceedings in Informatics, LIPIcs, 2018年, 査読有り

  
• Analytic functions and small complexity classes

  Florian Steinberg; Holger Thies

  CCA 2016 - 13th International Conference on Computability and Complexity in Analysis - Proceedings, 2016年

  
• Analytic functions in IrRAM

  Akitoshi Kawamura; Florian Steinberg; Holger Thies

  CCA 2014 - 11th International Conference on Computability and Complexity in Analysis, Proceedings, 2014年

  

外部資金：科学研究費補助金

• Computational complexity and practice of verified and efficient algorithms for dynamical systems

  若手研究

  小区分60010:情報学基礎論関連

  京都大学;九州大学

  THIES HOLGER

  自 2020年04月01日, 至 2025年03月31日, 完了

  Computable Analysis;Exact Real Computation;Complexity Theory;Formal Verification;Formal Proofs;Type Theory;ODEs;Program Extraction;Spaces of subsets;Proof Assistants;計算可能解析学;計算量;計算機援用証明;実数計算;Computable analysis;Differential equations;Verification;Formal proofs

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20K19744/
• 連続な空間上の計算とその複雑さの研究

  基盤研究(B)

  小区分60010:情報学基礎論関連

  京都大学

  立木 秀樹

  自 2023年04月01日, 至 2028年03月31日, 交付

  計算可能解析学;厳密実数計算;計算複雑さ;プログラム抽出

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23H03346/
• Research on Computable Analysis and Verification of Efficient Exact Real Computation

  若手研究

  小区分60010:情報学基礎論関連

  京都大学

  THIES HOLGER

  自 2024年04月01日, 至 2029年03月31日, 交付

  Formal Verification;Computable Analysis;Coq;Exact Real Computation;計算可能解析学;微分方程式;精度保証付き数値計算;計算機援用証明

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-24K20735/
• 連続な空間上の計算とその複雑さの研究

  基盤研究(B)

  小区分60010:情報学基礎論関連

  京都大学

  立木 秀樹

  自 2024年04月01日, 至 2028年03月31日, 交付

  計算可能解析学;厳密実数計算;計算複雑さ;プログラム抽出

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23K28036/

教育

担当科目

• 自 2025年04月01日, 至 2026年03月31日

  ILAS Seminar-E2

  Z002, 前期, 国際高等教育院, 2
• 自 2025年04月01日, 至 2026年03月31日

  学術越境基礎1

  M226, 前期, 国際高等教育院, 2
• 自 2025年04月01日, 至 2026年03月31日

  Programming Practice (Python) -E2

  T063, 前期, 国際高等教育院, 2
• 自 2025年04月01日, 至 2026年03月31日

  Programming Practice (Python) -E2

  T063, 後期, 国際高等教育院, 2
• 自 2025年04月01日, 至 2026年03月31日

  Information Network-E2

  T019, 後期, 国際高等教育院, 2
• 自 2025年04月01日, 至 2026年03月31日

  基礎演習：Introduction to Logic, Proofs and Programs

  8474, 前期, 総合人間学部, 2
• 自 2025年04月01日, 至 2026年03月31日

  数理・情報科学入門

  0060, 前期, 総合人間学部, 2
• 自 2025年04月01日, 至 2026年03月31日

  学術越境基礎1

  KK02, 前期, 人間・環境学研究科, 2
• 自 2024年04月01日, 至 2025年03月31日

  Programming Practice (Python) -E2

  T063, 前期, 国際高等教育院, 2
• 自 2024年04月01日, 至 2025年03月31日

  Programming Practice (Python) -E2

  T063, 後期, 国際高等教育院, 2
• 自 2024年04月01日, 至 2025年03月31日

  Information Network-E2

  T019, 後期, 国際高等教育院, 2
• 自 2024年04月01日, 至 2025年03月31日

  ILAS Seminar-E2

  Z002, 前期, 国際高等教育院, 2
• 自 2024年04月01日, 至 2025年03月31日

  基礎演習：Introduction to Logic, Proofs and Programs

  8474, 前期, 総合人間学部, 2
• 自 2024年04月01日, 至 2025年03月31日

  計算論

  8208, 前期, 総合人間学部, 2
• 自 2024年04月01日, 至 2025年03月31日

  数理・情報科学入門

  0060, 前期, 総合人間学部, 2
• 自 2024年04月01日, 至 2025年03月31日

  学術越境基礎1

  KK02, 前期, 人間・環境学研究科, 2
• 自 2024年04月01日, 至 2025年03月31日

  計算基礎論1

  AA21, 前期, 人間・環境学研究科, 2
• 自 2023年04月01日, 至 2024年03月31日

  ILAS Seminar-E2

  Z002, 前期, 国際高等教育院, 2
• 自 2023年04月01日, 至 2024年03月31日

  Programming Practice (Python) -E2

  T063, 前期, 国際高等教育院, 2
• 自 2023年04月01日, 至 2024年03月31日

  Programming Practice (Python) -E2

  T063, 後期, 国際高等教育院, 2
• 自 2023年04月01日, 至 2024年03月31日

  Information Network-E2

  T019, 後期, 国際高等教育院, 2
• 自 2023年04月01日, 至 2024年03月31日

  基礎演習：Introduction to Logic, Proofs and Programs

  8474, 前期, 総合人間学部, 2
• 自 2023年04月01日, 至 2024年03月31日

  数理情報論入門

  0057, 前期, 総合人間学部, 2
• 自 2023年04月01日, 至 2024年03月31日

  学術越境基礎1

  KK02, 前期, 人間・環境学研究科, 2
• 自 2022年04月01日, 至 2023年03月31日

  Programming Practice (Python) -E2

  T063, 後期, 国際高等教育院, 2
• 自 2022年04月01日, 至 2023年03月31日

  Programming Practice (Python) -E2

  T063, 前期, 国際高等教育院, 2
• 自 2022年04月01日, 至 2023年03月31日

  基礎演習：Introduction to Logic, Proofs and Programs

  8474, 前期, 総合人間学部, 2
• 自 2022年04月01日, 至 2023年03月31日

  数理情報論入門

  0057, 前期, 総合人間学部, 2
• 自 2022年04月01日, 至 2023年03月31日

  Information Network-E2

  T019, 後期, 国際高等教育院, 2
• 自 2022年04月01日, 至 2023年03月31日

  ILAS Seminar-E2

  Z002, 前期, 国際高等教育院, 2