Theory And Applications of Induction Recursion
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
(2009)
Indexed Containers
Hancock P
(2013)
Typed Lambda Calculi and Applications
Kraus N
(2017)
Notions of Anonymous Existence in Martin-L\"of Type Theory
Kraus N
(2016)
Notions of Anonymous Existence in Martin-Löf Type Theory
Mishra S
(2023)
'Cyclic syndrome' of arrears and efficiency of Indian judiciary.
in SN business & economics
Thorsten Altenkirch (Author)
(2010)
Higher-Order Containers
Thorsten Altenkirch (Author)
(2012)
A Syntactical Approach to Weak omega-Groupoids
Zhu J
(2022)
The Potential Protective Role of GS-441524, a Metabolite of the Prodrug Remdesivir, in Vaccine Breakthrough SARS-CoV-2 Infections.
in Intensive care research
| Description | We were looking at extensions of the container formalism (indexed containers and higher order containers) which are special cases of inductive-recursive definitions. We also proposed a categorical semantics for inductive-inductive definitions another variation on the project theme. We have shown that in some cases inductive-recursive definitions can be reduced to inductive-inductive definitions. |
| Exploitation Route | Our categorical semantics provided important impact to the study of Higher Inductive Types in the context of Homotopy Type Theory which is the subject of current research. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| URL | https://en.wikipedia.org/wiki/Induction-recursion |