1.  12
    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  
    Bookmark   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  
  4. Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf.Peter Dybjer, Sten Lindström, Erik Palmgren & B. Göran Sundholm - 2012 - Springer.
    This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice (ZFC). This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively (...)
    Export citation