Higher Algebra and Quantum Protocols

Lead Research Organisation: University of Birmingham
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.
 
Description Fundamental insight has been gained into the computational structure of higher-dimensional types, with emerging breakthrough applications to the foundations of programming languages and formalization of mathematics.
Exploitation Route Programming language design; research into pure mathematics.
Sectors Digital/Communication/Information Technologies (including Software)
 
Description Advising on quantum computing for governance
Geographic Reach National 
Policy Influence Type Influenced training of practitioners or researchers
 
Title Catt.io 
Description Software tool for working with syntactic expressions in higher category theory 
Type Of Technology New/Improved Technique/Technology 
Year Produced 2019 
Impact Accelerated research progress in this area of mathematics. 
URL https://arxiv.org/abs/1703.09050
 
Title Type theory allowing explicit construction of the infty-groupoid associated to any type 
Description An Agda implementation of the ideas from the paper Types are Internal 8-Groupoids, including an explicit construction of the 8-groupoid associated to any type, and a partial formalization of the equivalence with the type of all types. 
Type Of Technology Webtool/Application 
Year Produced 2021 
Open Source License? Yes  
Impact Substantial effect on the understanding in the foundations of computer science community of the groupoid structure of types. 
URL https://github.com/ericfinster/opetopic-types
 
Title homotopy.io 
Description Research tool for higher category theory 
Type Of Technology Webtool/Application 
Year Produced 2022 
Open Source License? Yes  
Impact Increased impact of scientific results in the community 
URL http://homotopy.io
 
Description Public engagement workshop 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Schools
Results and Impact Outreach activity
Year(s) Of Engagement Activity 2022
 
Description Qubit Zone public engagement workshop 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Public/other audiences
Results and Impact Public workshop that allows the general public to interact with quantum computer simulations. Have delivered it over 20 times to around 20-30 participants per event. Hugely successful ongoing outreach programme.
Year(s) Of Engagement Activity 2019,2020