ERC Consolidator Grant · 2024
Higher Observational Type Theory
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,…
From the public funding record at EU CORDIS. Describes the funded project, not the reviews below.