An easy to understand language for formal verification
Mathematics and computer science rely on formal verification to ensure the accuracy of reasoning and the safety of critical software. Recent advances, such as the formalisation of the four-colour theorem and verified components in Google’s Chrome browser, have showcased the power of proof assistants. These tools are built on the language of type theory. Despite its success in academia, Homotopy Type Theory (HoTT) has not seen widespread adoption due to its complex syntax and conceptual challenges. With this in mind, the ERC-funded HOTT project aims to develop a new type theory where homotopical content emerges naturally, simplifying the process. By defining equality types through computation, this project will make formalisation more accessible, accelerating progress in mathematics and software verification.
Objective
Recent advancements have enabled proof asistants 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 are formally verified parts of Google's Chrome web browser and verified implementations of the C and ML programming languages.
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, and elements of an equality type are paths in the space. Based one 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 being treated as the same.
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, bureaucractic process.
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 makes HoTT explainable and conceptually simple. It also improves pragmatic aspects: with more computation, proofs become less tedious. Our theory will contribute to a new era in formalisation of mathematics and verification of software, where developing proofs in abstract, reusable ways becomes standard, accelerating progress in both areas.
Keywords:
– Type heory
– Proof assistants
– Foundations of mathematics
– Logic
Host institution:
EOTVOS LORAND TUDOMANYEGYETEM (ELTE)
Principal Investigator, project leader: Dr. Ambrus Kaposi
Participating Departments: ELTE, Faculty of Informatics, Department of Programming Languages and Compliers.
The knowledge map of the Faculty
ERC HOTT – ERC-2024-COG – 101170308
Funded by the European Union. Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or European Research Council Executive Agency (ERCEA). Neither the European Union nor the granting authority can be held responsible for them.
