Jump to content

Induction-recursion

Add links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Lambiam (talk | contribs) at 23:56, 29 January 2013 (context in lead). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

In intuitionistic type theory (ITT), induction-recursion is a feature for declaring a type and function on that type. It allows the creation of larger types, such as universes, than inductive Types. The types created still remains predicative inside ITT.

Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, Journal of Symbolic Logic, Volume 65, Number 2, June 2000, pp 525-549.

A list of Peter Dybjer's publications on induction and induction-recursion

Retrieved from "https://en.wikipedia.org/w/index.php?title=Induction-recursion&oldid=535599463"