A general formulation of simultaneous inductive-recursive definitions in type theory

DOI10.2307/2586554zbMath0960.03048WikidataQ59540955 ScholiaQ59540955MaRDI QIDQ4508246

Peter Dybjer

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

zbMATH Keywords

Frege structures; intuitionistic type theory; simultaneous inductive-recursive definition

Mathematics Subject Classification ID

03F35: Second- and higher-order arithmetic and fragments

03D70: Inductive definability

Related Items

Dependent Types at Work, Program Testing and the Meaning Explanations of Intuitionistic Type Theory, Normalization by Evaluation for Martin-Löf Type Theory with One Universe, Map fusion for nested datatypes in intensional type theory, Viewing \({\lambda}\)-terms through maps, Partial and nested recursive function definitions in higher-order logic, Induction-recursion and initial algebras., Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory, Regular universes and formal spaces, Indexed induction-recursion, Another Look at Function Domains, A Brief Overview of Agda – A Functional Language with Dependent Types, Working with Mathematical Structures in Type Theory, Least and Greatest Fixpoints in Game Semantics, 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 ω

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