A finite axiomatization of inductive-recursive definitions
From MaRDI portal
Recommendations
- A finite axiomatisation of inductive-inductive definitions
- Inductive definitions over finite structures
- scientific article; zbMATH DE number 515737
- scientific article; zbMATH DE number 922631
- Infinitary logic and inductive definability over finite structures
- Recursive definitions and fixed-points on well-founded structures
- Equivalents of the finitary non-deterministic inductive definitions
- Inductive definitions over a predicative arithmetic
- Weak determinacy and iterations of inductive definitions
- On systems of definitions, induction and recursion
Cited in
(31)- Induction-recursion and initial algebras.
- Finitary higher inductive types in the groupoid model
- Constructing a universe for the setoid model
- Indexed induction-recursion
- Type-theoretic approaches to ordinals
- Type-level computation using narrowing in \(\Omega\)mega
- Turing-Completeness Totally Free
- Proof-producing reflection for HOL. With an application to model polymorphism
- How to reason coinductively informally
- Inductive-inductive definitions
- scientific article; zbMATH DE number 3985206 (Why is no real title available?)
- Indexed induction-recursion
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Models of type theory based on Moore paths
- A finite axiomatisation of inductive-inductive definitions
- Constructing higher inductive types as groupoid quotients
- A syntax for higher inductive-inductive types
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- POPLMark reloaded: mechanizing proofs by logical relations
- Variations on inductive-recursive definitions
- Dependent Types at Work
- Signatures and induction principles for higher inductive-inductive types
- Program testing and the meaning explanations of intuitionistic type theory
- scientific article; zbMATH DE number 3204589 (Why is no real title available?)
- Containers, monads and induction recursion
- A NOTE ON THEORIES FOR QUASI-INDUCTIVE DEFINITIONS
- For Finitary Induction-Induction, Induction is Enough
- Impredicative encodings of inductive-inductive data in Cedille
- A syntax for mutual inductive families
- Separating Markov's principles
- Why not \(\mathtt{W}\)?
This page was built for publication: A finite axiomatization of inductive-recursive definitions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263867)
