Deep induction for inductive families

DOI10.1007/978-3-031-99536-1_2MaRDI QIDQ6876469zbMATH OpenFDO

Authors Patricia Johann, Edward Morehouse

Publication date 13 January 2026

Full work available at URL https://doi.org/10.1007/978-3-031-99536-1_2

zbMATH Keywords

deep inductioninductive familiesproof assistants

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• Advanced Functional Programming
• Complete and decidable type inference for GADTs
• Deep induction: induction rules for (truly) nested types
• Dependently typed programming in Agda
• Guarded recursive datatype constructors
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• Inductive families
• Meta-programming with built-in type equality
• The view from the left

This page was built for publication: Deep induction for inductive families

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