1. 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.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2. Peter Dybjer & Anton Setzer (2003). Induction–Recursion and Initial Algebras. Annals of Pure and Applied Logic 124 (1-3):1-47.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  3. 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)  
     
    My bibliography  
     
    Export citation