Deep induction: induction rules for (truly) nested types

DOI10.1007/978-3-030-45231-5_18OpenAlexW3017064703MaRDI QIDQ2200833

Andrew Polonsky, Patricia Johann

Publication date: 23 September 2020

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

Mathematics Subject Classification ID

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

Related Items (2)

Unnamed Item ⋮ Parametricity for primitive nested types

Cites Work

• Unnamed Item
• Containers: Constructing strictly positive types
• Truly Modular (Co)datatypes for Isabelle/HOL
• Generic Fibrational Induction
• Fibrational Induction Rules for Initial Algebras
• An induction principle for nested datatypes in intensional type theory
• de Bruijn notation as a nested datatype
• Purely Functional Data Structures
• Indexed containers
• Automata, Languages and Programming
• Semi-continuous Sized Types and Termination

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