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.

Subsidie
€ 1.897.375
2025

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:

  1. Make HoTT explainable and conceptually simple
  2. 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

Startdatum1-5-2025
Einddatum30-4-2030
Subsidiejaar2025

Partners & Locaties

Projectpartners

  • EOTVOS LORAND TUDOMANYEGYETEMpenvoerder

Land(en)

Hungary

Vergelijkbare projecten binnen European Research Council

ERC Advanced...

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.

€ 2.499.776
ERC Consolid...

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.

€ 2.000.000
ERC Advanced...

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.

€ 2.227.500
ERC Starting...

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.

€ 989.395
ERC Starting...

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.

€ 1.470.201