Homotopy Type Theory: Programming and Verification
Lead Research Organisation:
University of Nottingham
Department Name: School of Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
People |
ORCID iD |
| Thorsten Altenkirch (Principal Investigator) |
Publications
Altenkirch T
(2020)
The Integers as a Higher Inductive Type
Altenkirch T
(2016)
Type theory in type theory using quotient inductive types
Altenkirch T
(2016)
Extending Homotopy Type Theory with Strict Equality
Altenkirch T
(2018)
Foundations of Software Science and Computation Structures
Altenkirch T.
(2016)
Normalisation by evaluation for dependent types
in Leibniz International Proceedings in Informatics, LIPIcs
Altenkirch Thorsten
(2017)
NORMALISATION BY EVALUATION FOR TYPE THEORY, IN TYPE THEORY
in LOGICAL METHODS IN COMPUTER SCIENCE
| Description | We have found new applications of concepts from Homotopy Type Theory in particular we have shown that QIITS (quotient inductive inductive types) can be used to present an internal intrinsic syntax for Type Theory and extend normalisation by evaluation, a technique to decide equality of terms, to this setting. We have also presented an extension of Homotopy Type Theory, a 2 level theory which allows us to talk about strict equalities, and are abel to show that one can use this to formalise the concept of semi-simplicial types which was not possible so far. This is an important stepping stone to solve so called coherence problems when working with proof-relevant equality. |
| Exploitation Route | Our research should feed into the design of new languages and tools using HoTT and support formal certification in general. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Description | The following is an impact summary for the Homotopy Type Theory grant of Ghani, Altenkirch, McBride and Gambino. The project had significant impact as follows Papers: Our paper of the use of HoTT to give better presentations of data types Constructing quotient inductive-inductive types, Free higher groups in homotopy type theory, The integers as a higher inductive type have become widely accepted as state of the art and influences the work of many other academics as well as programming language design, eg Cubical Agda (Sweden), REdPRL (USA). Our papers Type theory in type theory using quotient inductive types, Normalisation by evaluation for type theory, in type theory show how our work has been used to redefined the foundations of type theory using HoTT. Our papers Setoid type theory-a syntactic translation, Constructing a universe for the setoid model are spurred a project in Hungary investigating implementing a cut-down version HoTT, called setoid type theory. The paper [Towards a cubical type theory without an interval] is being used by Schulman on a project Higher Observational Type Theory. Gambino's work led to a partial solution to the one of the main open problems in Homotopy Type Theory, namely to what extent Voevodsky's simplicial model of Univalent Foundations can be developed constructively. In particular, Gambino, Henry, Sattler, Szumilo obtained a constructive version of the Kan-Quillen model structure, provided convenient conditions for having dependent products in homotopical models, leaving only a coherence issue to be addressed. This work was subsequently extended to construct new model structures, which are having an impact in the creation of a satisfactory definition of elementary higher topos. Another achievement is the development of new tools to test semantical validity of type-theoretic statements, via a refinement of the fundamental Kripke-Joyal semantics, which are currently being used by other researchers in HoTT. The paper Three Equivalent Ordinal Notation Systems in Cubical Agda applies HoTT to ordinal systems with one referee speculating the journal version might become the encyclopedic reference on ordinals in type theory in the future/. Education: The project had as an aim the education and training of others. Broad impact can be seen from courses delivered to invited summer schools, eg at the EUTypes Summer School on Types for Programming and Verification (2017: Thorsten Altenkirch; 2018: Fredrik Nordvall Forsberg; 2019: Nicolai Kraus). Conor McBride also gave a keynote talk at TYPES 2019 to the entire community about our variant of cubical type theory. Altenkirch presented at the Midland Graduate School which was attended in person by over hundred students. Altenkirch also presented invited lectures on Type Theory related to our project at the prestigious Oregon Summer School in 2022. Staff and PGR students on the project also got deeper training, eg the RA James Chapman has been using skills developed in his role at IOHK Edinburgh, RA Guillaume Alias has become a permanent academic, PGR student Kraus obtained a Royal Society Fellowship, PGR student Kaposi now leads his own research group, PGR students Capriotti and Orsanigo have become software developers, and Sattler is an RA at Chalmers. Software Development: The Platypus and ZEUG prototype implementations we developed explored the design space of cubical type theories, and influenced the development of other prototype languages such as RedTT, CoolTT, Cubical Agda and theoretical investigations such as XTT. They also influenced the system TypeOS currently being used in a Knowledge Exchange grant with the National Physical Laboratory on Units of Measure. Follow on Funding: Direct follow on funding includes Altenkirch's grant from the US AirForce "Certified Programming with Dependent Types" award FA9550-16-1-0029. |
| First Year Of Impact | 2020 |
| Sector | Digital/Communication/Information Technologies (including Software),Education,Other |
| Impact Types | Cultural,Economic |
| Description | Computer Science n Mathematics (Type Theory) - Computerphile (youtube) |
| Form Of Engagement Activity | A broadcast e.g. TV/radio/film/podcast (other than news/press) |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Public/other audiences |
| Results and Impact | As computers are used more and more to confirm proofs, is it time to take computer science's contribution to mathematics further? Dr Thorsten Altenkirch discusses Type Theory vs Set Theory. |
| Year(s) Of Engagement Activity | 2017 |
| URL | https://www.youtube.com/watch?v=qT8NyyRgLDQ |
| Description | Homotopy Type Theory: Vladimir Voevodsky - Computerphile |
| Form Of Engagement Activity | A broadcast e.g. TV/radio/film/podcast (other than news/press) |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Public/other audiences |
| Results and Impact | Voevodsky took his knowledge of abstract geometry and applied it to Computer Science, then took Computer Science principles and applied them to Mathematics. Professor Thorsten Altenkirch remembers him. |
| Year(s) Of Engagement Activity | 2017 |
| URL | https://www.youtube.com/watch?v=v5a5BYZwRx8 |
| Description | Introduction to homotopy type theory EU Types summer school , |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | Types are pervasive in programming and information technology. A type defines a formal interface between software components, allowing the automatic verification of their connections, and greatly enhancing the robustness and reliability of computations and communications. In rich dependent type theories, the full functional specification of a program can be expressed as a type. Type systems have rapidly evolved over the past years, becoming more sophisticated, capturing new aspects of the behaviour of programs and the dynamics of their execution. The aim of this summer school is to provide advanced training, especially to PhD students and early-career researchers, in all aspects of the theory and practice of type theory and applications. |
| Year(s) Of Engagement Activity | 2018 |
| URL | https://sites.google.com/view/summerschool2017-eutypes/home |
| Description | Propositions as Types - Computerphile |
| Form Of Engagement Activity | A broadcast e.g. TV/radio/film/podcast (other than news/press) |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Public/other audiences |
| Results and Impact | Mathematics once again meets Computer Science as Professor Altenkirch continues to discuss Type Theory |
| Year(s) Of Engagement Activity | 2017 |
| URL | https://www.youtube.com/watch?v=SknxggwRPzU |
| Description | Why Type Theory matters, Lambda Days 2019 |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | Why Type Theory matters Modern Type Theory (usually called Homotopy Type Theory) is at the same time the ultimate functional programming language and a novel foundation of Mathematics, an alternative to the mathematical assembly language called set theory. Type theory exploits the advantages of static typing to the limit, meaning that by hiding implementation details you can identify tow object which behave the same - this is called the univalence principle. |
| Year(s) Of Engagement Activity | 2019 |
| URL | http://www.lambdadays.org/lambdadays2019/thorsten-altenkirch |