Indexed containers

DOI10.1017/S095679681500009XzbMath1420.68032WikidataQ61583703 ScholiaQ61583703MaRDI QIDQ5371943

Peter G. Hancock, Thorsten Altenkirch, Peter A. Morris, Neil Ghani, Conor McBride

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s095679681500009x

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

Related Items

Unnamed Item, Unnamed Item, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs, Unnamed Item, Directed Containers as Categories, Variations on inductive-recursive definitions, Indexed containers, Interactive programming in Agda – Objects and graphical user interfaces, The essence of ornaments, Unnamed Item, 2-Dimensional Directed Type Theory, Subtyping without reduction, Characterizing functions mappable over GADTs, For Finitary Induction-Induction, Induction is Enough, A formalized general theory of syntax with bindings: extended version, Deep induction: induction rules for (truly) nested types, From Proposition to Program, Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract), Data Types with Symmetries and Polynomial Functors over Groupoids, How to Reason Coinductively Informally

Uses Software

• Agda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the greatest fixed point of a set functor
• Normal functors, power series and \(\lambda\)-calculus
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Containers: Constructing strictly positive types
• Programming interfaces and basic topology
• Indexed induction-recursion
• Positive Inductive-Recursive Definitions
• A Categorical Semantics for Inductive-Inductive Definitions
• Monads Need Not Be Endofunctors
• Subtyping, Declaratively
• Higher-Order Containers
• Inductive-Inductive Definitions
• Subset Coercions in Coq
• A UNIVERSE OF STRICTLY POSITIVE FAMILIES
• Big-step normalisation
• A construction of non-well-founded sets within Martin-Löf's type theory
• The Zipper
• Conservativity of equality reflection over intensional type theory
• A set constructor for inductive sets in Martin-Löf's type theory
• The gentle art of levitation
• Small Induction Recursion
• Indexed containers
• The cartesian closed bicategory of generalised species of structures
• Types for Proofs and Programs