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)

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

Related Items

Indexed containers, Interactive programming in Agda – Objects and graphical user interfaces, The essence of ornaments, 2-Dimensional Directed Type Theory, 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

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