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.

Publications

10 25 50
publication icon
Altenkirch T (2009) Indexed Containers

publication icon
Hancock P (2013) Typed Lambda Calculi and Applications

publication icon
Kraus Nicolai (2017) NOTIONS OF ANONYMOUS EXISTENCE IN MARTIN-LOF TYPE THEORY in LOGICAL METHODS IN COMPUTER SCIENCE

publication icon
Mishra S (2023) 'Cyclic syndrome' of arrears and efficiency of Indian judiciary. in SN business & economics

publication icon
Thorsten Altenkirch (Author) (2012) A Syntactical Approach to Weak omega-Groupoids

publication icon
Thorsten Altenkirch (Author) (2010) Higher-Order Containers

publication icon
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