Jump to content

Induction-recursion

Add links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Mdnahas (talk | contribs) at 19:15, 29 January 2013 (Creating page on induction-recursion). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.
(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

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


Peter Dybner, 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=535559352"