1.  8
    Peter Dybjer & Denis Kuperberg (2012). Formal Neighbourhoods, Combinatory Böhm Trees, and Untyped Normalization by Evaluation. Annals of Pure and Applied Logic 163 (2):122-131.
  2.  6
    Peter Dybjer (2000). A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. 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 (6 more)  
    Export citation  
    My bibliography   3 citations  
  3. Peter Dybjer & Anton Setzer (2003). Induction–Recursion and Initial Algebras. 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