Higher Observational Type Theory
This project aims to create an innovative type theory that simplifies homotopy type theory by defining equality through computation, enhancing mathematical formalization and software verification.
Projectdetails
Introduction
Recent advancements have enabled proof assistants to formally verify world-class mathematics: the liquid tensor experiment, the four colour theorem, and the odd order theorem were formalised. Computer-checked arguments are important for mathematicians who want to be certain their reasoning is sound, and for computer scientists to prevent bugs in safety-critical software. Examples include formally verified parts of Google's Chrome web browser and verified implementations of the C and ML programming languages.
Type Theory and Its Importance
At the core of these formalisations lies type theory, upon which proof assistants are built. Type theory is both a functional programming language and a foundation of mathematics. Recently, models of type theory built on higher-dimensional spaces emerged, where:
- Elements of a type are points in the space
- Elements of an equality type are paths in the space
Based on these, type theory was extended to homotopy type theory (HoTT), featuring the principle that isomorphic types are equal. This moves formalisation close to actual mathematical practice, where isomorphic structures are treated as the same.
Challenges in Adoption
While HoTT is successful among academics, it hasn't been widely adopted. This is because type theories implementing HoTT rely on an explicit syntax for higher-dimensional geometry, which is conceptually difficult and hard to use in practice. This creates a substantial barrier for formalisation, which is treated as a low-level, bureaucratic process.
Project Goals
Our project will develop a radically new type theory where homotopical content is emergent, rather than built-in. The idea is to define the equality type via computation. This approach will:
- Make HoTT explainable and conceptually simple
- Improve pragmatic aspects, making proofs less tedious
Our theory will contribute to a new era in the formalisation of mathematics and verification of software, where developing proofs in abstract, reusable ways becomes standard, accelerating progress in both areas.
Financiële details & Tijdlijn
Financiële details
Subsidiebedrag | € 1.897.375 |
Totale projectbegroting | € 1.897.375 |
Tijdlijn
Startdatum | 1-5-2025 |
Einddatum | 30-4-2030 |
Subsidiejaar | 2025 |
Partners & Locaties
Projectpartners
- EOTVOS LORAND TUDOMANYEGYETEMpenvoerder
Land(en)
Vergelijkbare projecten binnen European Research Council
Project | Regeling | Bedrag | Jaar | Actie |
---|---|---|---|---|
Formalisation of Constructive Univalent Type TheoryThe project aims to explore the correspondence between dependent type theory and homotopy theory to develop new mathematical foundations and enhance proof systems for complex software and proofs. | ERC Advanced... | € 2.499.776 | 2022 | Details |
Realizing the Promise of Higher-Order SMT and Superposition for Interactive VerificationThe Nekoka project aims to enhance higher-order SMT and λ-superposition for automated proof assistance, integrating them into tools for software verification and mathematical formalization. | ERC Consolid... | € 2.000.000 | 2023 | Details |
Logics and Algorithms for a Unified Theory of HyperpropertiesThis project aims to develop a unified theory and formal tools for hyperproperties in software, focusing on societal values like privacy and fairness, to enhance program verification and synthesis. | ERC Advanced... | € 2.227.500 | 2022 | Details |
Definable Algebraic TopologyThis project aims to enhance algebraic topology and coarse geometry by integrating Polish covers with homological invariants, leading to new classification methods and insights in mathematical logic. | ERC Starting... | € 989.395 | 2023 | Details |
Motivic Stable Homotopy Theory: a New Foundation and a Bridge to p-Adic and Complex GeometryThis project aims to advance cohomology theories in algebraic and analytic geometry through innovations in motivic stable homotopy theory, enhancing connections with p-adic and complex geometry. | ERC Starting... | € 1.470.201 | 2025 | Details |
Formalisation of Constructive Univalent Type Theory
The project aims to explore the correspondence between dependent type theory and homotopy theory to develop new mathematical foundations and enhance proof systems for complex software and proofs.
Realizing the Promise of Higher-Order SMT and Superposition for Interactive Verification
The Nekoka project aims to enhance higher-order SMT and λ-superposition for automated proof assistance, integrating them into tools for software verification and mathematical formalization.
Logics and Algorithms for a Unified Theory of Hyperproperties
This project aims to develop a unified theory and formal tools for hyperproperties in software, focusing on societal values like privacy and fairness, to enhance program verification and synthesis.
Definable Algebraic Topology
This project aims to enhance algebraic topology and coarse geometry by integrating Polish covers with homological invariants, leading to new classification methods and insights in mathematical logic.
Motivic Stable Homotopy Theory: a New Foundation and a Bridge to p-Adic and Complex Geometry
This project aims to advance cohomology theories in algebraic and analytic geometry through innovations in motivic stable homotopy theory, enhancing connections with p-adic and complex geometry.