Deep induction: induction rules for (truly) nested types

DOI10.1007/978-3-030-45231-5_18MaRDI QIDQ2200833zbMATH OpenOpenAlexFDO

Authors Patricia Johann, Andrew Polonsky

Publication date 23 September 2020

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-45231-5_18

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Recommendations

• An induction principle for nested datatypes in intensional type theory
• Fibrational induction rules for initial algebras
• Generic fibrational induction
• Recursion on Nested Datatypes in Dependent Type Theory
• A principled approach to programming with nested types in Haskell

Cites work

• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• An induction principle for nested datatypes in intensional type theory
• Automata, Languages and Programming
• Containers: Constructing strictly positive types
• Fibrational induction rules for initial algebras
• Generic fibrational induction
• Indexed containers
• Purely Functional Data Structures
• Semi-continuous Sized Types and Termination
• Truly modular (co)datatypes for Isabelle/HOL
• de Bruijn notation as a nested datatype

Cited in

(4)

• Parametricity for primitive nested types
• scientific article; zbMATH DE number 7471683 (Why is no real title available?)
• GADTs, functoriality, parametricity: pick two
• scientific article; zbMATH DE number 7668098 (Why is no real title available?)

This page was built for publication: Deep induction: induction rules for (truly) nested types

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