Containers: Constructing strictly positive types

DOI10.1016/j.tcs.2005.06.002zbMath1077.68015OpenAlexW2079640625WikidataQ61583925 ScholiaQ61583925MaRDI QIDQ2566024

Yanyan Li

Publication date: 22 September 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.06.002

zbMATH Keywords

InductionCategory theoryInitial algebrasType theoryCoinductionContainer functorsFinal coalgebrasW-Types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (42)

Generic recursive lens combinators and their calculation laws ⋮ Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract) ⋮ Proving Properties about Functions on Lists Involving Element Tests ⋮ Coalgebraic update lenses ⋮ Homotopical patch theory ⋮ Partiality and Container Monads ⋮ Data Types with Symmetries and Polynomial Functors over Groupoids ⋮ The costructure–cosemantics adjunction for comodels for computational effects ⋮ Complexity bounds for container functors and comonads ⋮ Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ Unnamed Item ⋮ Quotienting the delay monad by weak bisimilarity ⋮ Non-well-founded trees in categories ⋮ A Mechanized Theory of Regular Trees in Dependent Type Theory ⋮ Directed Containers as Categories ⋮ Universal properties of bicategories of polynomials ⋮ Protocol choice and iteration for the free cornering ⋮ Characterizing functions mappable over GADTs ⋮ Deep induction: induction rules for (truly) nested types ⋮ Coalgebras in functional programming and type theory ⋮ Unnamed Item ⋮ Indexed containers ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Friends with Benefits ⋮ A Syntax for Higher Inductive-Inductive Types ⋮ Galois Connections for Recursive Types ⋮ Decomposing Comonad Morphisms. ⋮ Polynomial functors and polynomial monads ⋮ A linear category of polynomial diagrams ⋮ W-types in homotopy type theory ⋮ Containers, monads and induction recursion ⋮ Unnamed Item ⋮ Incremental Computing with Abstract Data Structures ⋮ Continuous Functions on Final Coalgebras ⋮ A UNIVERSE OF STRICTLY POSITIVE FAMILIES ⋮ A Coalgebraic View of Bar Recursion and Bar Induction ⋮ Modular Dependent Induction in Coq, Mendler-Style ⋮ The universal exponentiable arrow ⋮ Variations on inductive-recursive definitions ⋮ Constructive Membership Predicates as Index Types ⋮ Comonadic Notions of Computation

Uses Software

• Epigram

Cites Work

• Non-well-founded trees in categories
• Categorical logic and type theory
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Wellfounded trees in categories
• Generalised folds for nested datatypes
• Locally cartesian closed categories and type theory
• Fibered categories and the foundations of naive category theory
• Categories for Types
• Container types categorically
• Extensional Constructs in Intensional Type Theory
• The view from the left
• Mathematics of Program Construction
• Advanced Functional Programming
• Automata, Languages and Programming
• Types for Proofs and Programs
• Two applications of analytic functors
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Containers: Constructing strictly positive types