1.  11
    A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory.Peter Dybjer - 2000 - Journal of Symbolic Logic 65 (2):525-549.
    The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löf's universe á la Tarski. A set U 0 of codes for small sets is generated inductively at the same time as a function T 0 , which maps a code to the corresponding small set, is defined by recursion on the way the elements of U 0 are generated. In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition which is (...)
    Direct download (8 more)  
    Export citation  
    My bibliography   3 citations  
  2.  16
    Formal Neighbourhoods, Combinatory Böhm Trees, and Untyped Normalization by Evaluation.Peter Dybjer & Denis Kuperberg - 2012 - Annals of Pure and Applied Logic 163 (2):122-131.
  3.  3
    Induction–Recursion and Initial Algebras.Peter Dybjer & Anton Setzer - 2003 - Annals of Pure and Applied Logic 124 (1-3):1-47.
    Induction–recursion is a powerful definition method in intuitionistic type theory. It extends inductive definitions and allows us to define all standard sets of Martin-Löf type theory as well as a large collection of commonly occurring inductive data structures. It also includes a variety of universes which are constructive analogues of inaccessibles and other large cardinals below the first Mahlo cardinal. In this article we give a new compact formalization of inductive–recursive definitions by modeling them as initial algebras in slice categories. (...)
    Direct download (3 more)  
    Export citation  
    My bibliography