Map fusion for nested datatypes in intensional type theory

DOI10.1016/j.scico.2010.05.008zbMath1210.68048OpenAlexW2018045457MaRDI QIDQ627204

Ralph Matthes

Publication date: 21 February 2011

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2010.05.008

zbMATH Keywords

type theoryCoqdatatypes with true nestingexplicit flatteningmonad laws for substitutionnaturality for generalized mapsterminating recursion schemes

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Data structures (68P05)

Related Items (4)

Unnamed Item ⋮ Parametricity for primitive nested types ⋮ Modular Dependent Induction in Coq, Mendler-Style ⋮ Heterogeneous Substitution Systems Revisited

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A principled approach to programming with nested types in Haskell
• Substitution: A formal methods case study using monads and transformations
• Iteration and coiteration schemes for higher-order and nested datatypes
• Disciplined, efficient, generalised folds for nested datatypes
• Generalised folds for nested datatypes
• Recursion on Nested Datatypes in Dependent Type Theory
• Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening
• An induction principle for nested datatypes in intensional type theory
• de Bruijn notation as a nested datatype
• Type-based termination of recursive definitions
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Generalizing generalized tries
• Computer Science Logic

This page was built for publication: Map fusion for nested datatypes in intensional type theory