Positive inductive-recursive definitions
From MaRDI portal
Publication:2848936
DOI10.1007/978-3-642-40206-7_3zbMATH Open1395.68189OpenAlexW2901304827MaRDI QIDQ2848936FDOQ2848936
Authors: Neil Ghani, Lorenzo Malatesta, Fredrik Nordvall Forsberg
Publication date: 13 September 2013
Published in: Algebra and Coalgebra in Computer Science (Search for Journal in Brave)
Full work available at URL: https://strathprints.strath.ac.uk/52999/
Recommendations
Theories (e.g., algebraic theories), structure, and semantics (18C10) Abstract data types; algebraic specification (68Q65)
Cited In (12)
- Finitary higher inductive types in the groupoid model
- Small induction recursion
- A categorical semantics for inductive-inductive definitions
- Constructing a universe for the setoid model
- Title not available (Why is that?)
- Indexed induction-recursion
- Indexed containers
- Fibred data types
- Positive inductive-recursive definitions
- Variations on inductive-recursive definitions
- Impredicative encodings of inductive-inductive data in Cedille
- For Finitary Induction-Induction, Induction is Enough
This page was built for publication: Positive inductive-recursive definitions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2848936)