Variations on inductive-recursive definitions

DOI10.4230/LIPIcs.MFCS.2017.63zbMath1445.03010OpenAlexW2768213019MaRDI QIDQ5111280

Stephan Spahn, Neil Ghani, Fredrik Nordvall Forsberg, Conor McBride

Publication date: 26 May 2020

Full work available at URL: https://doi.org/10.4230/lipics.mfcs.2017.63

zbMATH Keywords

type theoryinduction-recursioninitial-algebra semantics

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Type theory (03B38)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dependently typed records in type theory
• Inductive families
• Induction-recursion and initial algebras.
• Containers: Constructing strictly positive types
• Indexed induction-recursion
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Polynomial functors and polynomial monads
• The gentle art of levitation
• Indexed containers
• Types for Proofs and Programs
• Containers, monads and induction recursion

This page was built for publication: Variations on inductive-recursive definitions