Indexed containers

DOI10.1017/S095679681500009XzbMath1420.68032DBLPjournals/jfp/AltenkirchGHMM15OpenAlexW4240072532WikidataQ61583703 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

Related Items (20)

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

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

This page was built for publication: Indexed containers