Inductive-inductive definitions

DOI10.1007/978-3-642-15205-4_35MaRDI QIDQ3586059zbMATH OpenOpenAlexFDO

Authors Fredrik Nordvall Forsberg, Anton Setzer

Publication date 3 September 2010

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://cronfa.swan.ac.uk/Record/cronfa43083

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• A finite axiomatisation of inductive-inductive definitions
• A categorical semantics for inductive-inductive definitions
• Indexed induction-recursion
• scientific article; zbMATH DE number 2006633
• scientific article; zbMATH DE number 1342277

Cited in

(17)

• Non-deterministic inductive definitions
• Finitary higher inductive types in the groupoid model
• Intuitionistic fixed point logic
• Constructing inductive-inductive types in cubical type theory
• A categorical semantics for inductive-inductive definitions
• A general formulation of simultaneous inductive-recursive definitions in type theory
• ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS
• A finite axiomatisation of inductive-inductive definitions
• Constructing higher inductive types as groupoid quotients
• A syntax for higher inductive-inductive types
• On generalized algebraic theories and categories with families
• Indexed containers
• Interactive programming in Agda -- objects and graphical user interfaces
• Normalization by evaluation for modal dependent type theory
• For Finitary Induction-Induction, Induction is Enough
• Impredicative encodings of inductive-inductive data in Cedille
• Viewing \({\lambda}\)-terms through maps

Describes a project that uses

Uses Software

• Agda

This page was built for publication: Inductive-inductive definitions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3586059)