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.
Organisations
Publications
Anel Mathieu
(2017)
A Generalized Blakers-Massey Theorem
in arXiv e-prints
Finster E
(2021)
A Type Theory for Strictly Associative Infinity Categories
Finster E
(2022)
A Type Theory for Strictly Unital 8-Categories
Finster E
(2020)
A Type Theory for Strictly Unital Infty-Categories
Joyal A
(2021)
Higher Sheaves and Left-Exact Localizations of Infty-Topoi
Verdon D
(2019)
Quantum teleportation with infinite reference-frame uncertainty
in Physical Review A
Reutter DJ
(2019)
Shaded tangles for the design and verification of quantum circuits.
in Proceedings. Mathematical, physical, and engineering sciences
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 |