THIES HOLGER ＴＨＩＥＳＨＯＬＧＥＲ

Researcher Number	50839107
Other IDs
Affiliation (Current)	2025: 京都大学, 人間・環境学研究科, 特定講師
Affiliation (based on the past Project Information) *help	2021 – 2024: 京都大学, 人間・環境学研究科, 特定講師 2020: 九州大学, システム情報科学研究院, 助教
Review Section/Research Field	Principal Investigator Basic Section 60010:Theory of informatics-related Except Principal Investigator Sections That Are Subject to Joint Review: Basic Section60010:Theory of informatics-related , Basic Section60020:Mathematical informatics-related / Basic Section 60020:Mathematical informatics-related / Basic Section 60010:Theory of informatics-related
Keywords	Principal Investigator 計算機援用証明 / 計算可能解析学 / 精度保証付き数値計算 / 微分方程式 / Complexity Theory / Formal proofs / Verification / Differential equations / Computable analysis / 実数計算 … More / 計算量 / Proof Assistants / Spaces of subsets / Program Extraction / ODEs / Type Theory / Formal Proofs / Exact Real Computation / Computable Analysis … More Except Principal Investigator プログラム抽出 / 計算複雑さ / 厳密実数計算 / 計算可能解析学 Less

Research on Computable Analysis and Verification of Efficient Exact Real ComputationPrincipal Investigator
- Principal Investigator
  
  THIES HOLGER
- Project Period (FY)
  2024 – 2028
- Research Category
  
  Grant-in-Aid for Early-Career Scientists
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Kyoto University
連続な空間上の計算とその複雑さの研究
- Principal Investigator
  
  立木秀樹
- Project Period (FY)
  2023 – 2027
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
  Basic Section 60020:Mathematical informatics-related
  Sections That Are Subject to Joint Review: Basic Section60010:Theory of informatics-related , Basic Section60020:Mathematical informatics-related
- Research Institution
  Kyoto University
Computational complexity and practice of verified and efficient algorithms for dynamical systemsPrincipal Investigator
- Principal Investigator
  
  THIES HOLGER
- Project Period (FY)
  2020 – 2024
- Research Category
  
  Grant-in-Aid for Early-Career Scientists
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Kyoto University
  Kyushu University

All 2024 2023 2022 2021 2020

All Journal Article Presentation

[Journal Article] Formalizing Hyperspaces for Extracting Efficient Exact Real Computation2023
- Author(s)
  Michal Konecny, Sewon Park, Holger Thies
- Journal Title
  
  Leibniz International Proceedings in Informatics (LIPIcs)
  
  Volume: 272
- Data Source
  KAKENHI-PROJECT-20K19744
[Journal Article] Certified Computation of Nondeterministic Limits2022
- Author(s)
  Konecny Michal、Park Sewon、Thies Holger
- Journal Title
  
  Lecture Notes in Computer Science book series (LNCS)
  
  Volume: 13260 Pages: 771-789
- DOI
  10.1007/978-3-031-06773-0_41
- ISBN
  9783031067723, 9783031067730
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744, KAKENHI-PROJECT-18H03203
[Journal Article] Computable analysis and notions of continuity in Coq2021
- Author(s)
  Florian Steinberg, Laurent Thery, Holger Thies
- Journal Title
  
  Logical Methods in Computer Science
  
  Volume: 17:2
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Journal Article] Axiomatic Reals and Certified Efficient Exact Real Computation2021
- Author(s)
  Konecny Michal、Park Sewon、Thies Holger
- Journal Title
  
  Lecture Notes in Computer Science
  
  Volume: 13038 Pages: 252-268
- DOI
  10.1007/978-3-030-88853-4_16
- ISBN
  9783030888527, 9783030888534
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Journal Article] Exact Real Computation of Solution Operators for Linear Analytic Systems of Partial Differential Equations2021
- Author(s)
  Selivanova Svetlana、Steinberg Florian、Thies Holger、Ziegler Martin
- Journal Title
  
  Lecture Notes in Computer Science
  
  Volume: 12865 Pages: 370-390
- DOI
  10.1007/978-3-030-85165-1_21
- ISBN
  9783030851644, 9783030851651
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Journal Article] Continuous and Monotone Machines2020
- Author(s)
  Michal Konecny, Florian Steinberg, Holger Thies
- Journal Title
  
  Leibniz International Proceedings in Informatics (LIPIcs)
  
  Volume: 170
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Journal Article] Computable Analysis for Verified Exact Real Computation2020
- Author(s)
  Michal Konecny, Florian Steinberg, Holger Thies
- Journal Title
  
  Leibniz International Proceedings in Informatics (LIPIcs)
  
  Volume: 182
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Applications of Exact Real Computation in Particle Physics2024
- Author(s)
  Svetlana Selivanova, Holger Thies
- Organizer
  17th International Conference on Computability, Complexity and Randomness
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Extending cAERN to spaces of subsets2023
- Author(s)
  Michal Konecny, Sewon Park, Holger Thies
- Organizer
  29th International Conference on Types for Proofs and Programs
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Advances in verified set and function calculi in Coq2023
- Author(s)
  Pieter Collins, Sewon Park, Holger Thies
- Organizer
  Continuity, Computability, Constructivity 2023
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] 計算可能解析学とCoq2023
- Author(s)
  Holger Thies
- Organizer
  The 19th Theorem Proving and Provers meeting
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Towards verified implementation of iterative and interactive real-RAM2023
- Author(s)
  Sewon Park, Holger Thies
- Organizer
  Twentieth International Conference on Computability and Complexity in Analysis
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Formal verification and program extraction for efficient computations over real numbers and hyperspaces2023
- Author(s)
  Holger Thies
- Organizer
  Fifth Workshop on Digitalization and Computable Models
- Invited
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Certified exact real computation on hyperspaces2022
- Author(s)
  Michal Konecny, Sewon Park, Holger Thies
- Organizer
  Continuity, Computability, Constructivity - From Logic to Algorithm (CCC2022)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] From Coq Proofs to Efficient Certified Exact Real Computation2022
- Author(s)
  Michal Konecny, Sewon Park, Holger Thies
- Organizer
  Proof and Computation 2022
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Nondeterministic limits and certified exact real computation2022
- Author(s)
  Michal Konecny, Sewon Park, Holger Thies
- Organizer
  Nineteenth International Conference on Computability and Complexity in Analysis
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Extracting exact real computation programs from proofs in type theory2022
- Author(s)
  Holger Thies
- Organizer
  The second Japan-Russia workshop on effective descriptive set theory, computable analysis and automata
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Certified and efficient programs from proofs in computable analysis2022
- Author(s)
  Holger Thies
- Organizer
  Computing in topological structures: Foundations and implementations
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] An application of constructive dependent type theory to certified computation over the reals2022
- Author(s)
  Holger Thies
- Organizer
  The second Korea Logic Day
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Some steps toward program extraction in a type-theoretical interpretation of IFP2022
- Author(s)
  Ulrich Berger, Sewon Park, Holger Thies, Hideki Tsuiki
- Organizer
  Continuity, Computability, Constructivity - From Logic to Algorithm (CCC2022)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Toward an interpretation of Intutionistic Fixed Point Logic in Coq2021
- Author(s)
  Holger Thies
- Organizer
  The 17th Theorem Proving and Provers meeting
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Axiomatic Reals and Certified Efficient Exact Real Computatio2021
- Author(s)
  Holger Thies
- Organizer
  27th Workshop on Logic, Language, Information and Computation
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Complexity Theory in Analysis with Applications to Differential Equations2021
- Author(s)
  Holger Thies
- Organizer
  Autumn school Proof and Computatio
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Uniform Complexity of Solving Partial Differential Equations and Exact Real Computation2021
- Author(s)
  Holger Thies
- Organizer
  18th International Conference on Computability and Complexity in Analysis
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] IFP style proofs in the Coq proof assistant2021
- Author(s)
  Holger Thies
- Organizer
  Continuity, Computability, Constructivity - From Logic to Algorithm
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Computable Analysis for Verified Exact Real Computation2020
- Author(s)
  Holger Thies
- Organizer
  40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Continuous and Monotone Machines2020
- Author(s)
  Holger Thies
- Organizer
  45th International Symposium on Mathematical Foundations of Computer Science
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744
[Presentation] Computable analysis and exact real computation in Coq2020
- Author(s)
  Holger Thies
- Organizer
  Fourth Workshop on Mathematical Logic and Applications
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K19744

1. 立木秀樹 (10211377)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
2. 河村彰星 (20600117)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
3. 木原貴行 (80722701)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results

THIES HOLGER ＴＨＩＥＳ ＨＯＬＧＥＲ

Research Projects

Research Products

Co-Researchers

Research on Computable Analysis and Verification of Efficient Exact Real ComputationPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

連続な空間上の計算とその複雑さの研究

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Computational complexity and practice of verified and efficient algorithms for dynamical systemsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

[Journal Article] Formalizing Hyperspaces for Extracting Efficient Exact Real Computation2023

Author(s)

Journal Title

Data Source

[Journal Article] Certified Computation of Nondeterministic Limits2022

Author(s)

Journal Title

DOI

ISBN

Data Source

[Journal Article] Computable analysis and notions of continuity in Coq2021

Author(s)

Journal Title

Data Source

[Journal Article] Axiomatic Reals and Certified Efficient Exact Real Computation2021

Author(s)

Journal Title

DOI

ISBN

Data Source

[Journal Article] Exact Real Computation of Solution Operators for Linear Analytic Systems of Partial Differential Equations2021

Author(s)

Journal Title

DOI

ISBN

Data Source

[Journal Article] Continuous and Monotone Machines2020

Author(s)

Journal Title

Data Source

[Journal Article] Computable Analysis for Verified Exact Real Computation2020

Author(s)

Journal Title

Data Source

[Presentation] Applications of Exact Real Computation in Particle Physics2024

Author(s)

Organizer

Data Source

[Presentation] Extending cAERN to spaces of subsets2023

Author(s)

Organizer

Data Source

[Presentation] Advances in verified set and function calculi in Coq2023

Author(s)

Organizer

Data Source

[Presentation] 計算可能解析学とCoq2023

Author(s)

Organizer

Data Source

[Presentation] Towards verified implementation of iterative and interactive real-RAM2023

Author(s)

Organizer

Data Source

[Presentation] Formal verification and program extraction for efficient computations over real numbers and hyperspaces2023

Author(s)

Organizer

Data Source

THIES HOLGER ＴＨＩＥＳＨＯＬＧＥＲ