Variations on inductive-recursive definitions

DOI10.4230/LIPICS.MFCS.2017.63zbMATH Open1445.03010OpenAlexW2768213019MaRDI QIDQ5111280FDOQ5111280

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

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

Cites Work

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

Cited In (1)

• Comparing inductive and circular definitions: Parameters, complexity and games

   Recommendations

• Iterated Inductive Definitions Revisited 👍 👎
• On systems of definitions, induction and recursion 👍 👎
• On the complexity of inductive definitions 👍 👎
• Recursive Definitions and Fixed-Points 👍 👎
• Positive Inductive-Recursive Definitions 👍 👎
• Positive Inductive-Recursive Definitions 👍 👎
• Title not available (Why is that?) 👍 👎
• A note on multiple inductive definitions 👍 👎
• Non-deterministic inductive definitions 👍 👎
• Title not available (Why is that?) 👍 👎

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111280)