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:53, 29 January 2013 (sp). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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 Intuitionistic Type Theory.

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=535599053"