A general formulation of simultaneous inductive-recursive definitions in type theory
From MaRDI portal
Publication:4508246
DOI10.2307/2586554zbMath0960.03048OpenAlexW2058174669WikidataQ59540955 ScholiaQ59540955MaRDI QIDQ4508246
Publication date: 3 October 2000
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2586554
Related Items (40)
From type theory to setoids and back ⋮ Finitary higher inductive types in the groupoid model ⋮ From realizability to induction via dependent intersection ⋮ A Brief Overview of Agda – A Functional Language with Dependent Types ⋮ Unnamed Item ⋮ Working with Mathematical Structures in Type Theory ⋮ Normalization by evaluation for modal dependent type theory ⋮ A Comparison of Type Theory with Set Theory ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Map fusion for nested datatypes in intensional type theory ⋮ An intuitionistic set-theoretical model of fully dependent CC ⋮ Induction-recursion and initial algebras. ⋮ Pure type systems with explicit substitutions ⋮ Well-founded recursion with copatterns and sized types ⋮ Unnamed Item ⋮ A Syntax for Higher Inductive-Inductive Types ⋮ Constructing a universe for the setoid model ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ Containers, monads and induction recursion ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Dependent Types at Work ⋮ Unnamed Item ⋮ Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory ⋮ Least and Greatest Fixpoints in Game Semantics ⋮ Another Look at Function Domains ⋮ Viewing \({\lambda}\)-terms through maps ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ An induction principle for nested datatypes in intensional type theory ⋮ Typed Applicative Structures and Normalization by Evaluation for System F ω ⋮ Canonicity for cubical type theory ⋮ Unnamed Item ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ Variations on inductive-recursive definitions ⋮ Predicativity and constructive mathematics ⋮ Unnamed Item ⋮ Program Testing and the Meaning Explanations of Intuitionistic Type Theory ⋮ Regular universes and formal spaces ⋮ Indexed induction-recursion ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ Normalization by Evaluation for Martin-Löf Type Theory with One Universe
Cites Work
- Unnamed Item
- Propositional functions and families of types
- Inaccessibility in constructive set theory and type theory
- Inductive families
- Intuitionistic model constructions and normalization proofs
- The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
- Normalization and the Yoneda embedding
- A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS
This page was built for publication: A general formulation of simultaneous inductive-recursive definitions in type theory
