Deep induction: induction rules for (truly) nested types

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

Authors: Patricia Johann, Andrew Polonsky 

Publication date: 23 September 2020

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

• Parametricity for primitive nested types
• Title not available (Why is that?)
• GADTs, functoriality, parametricity: pick two
• Title not available (Why is that?)

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)