Representing nested inductive types using W-types

DOI10.1007/978-3-540-27836-8_8MaRDI QIDQ5466528zbMATH OpenOpenAlexFDO

Authors Michael Barry Abbott, Thorsten Altenkirch, Neil Ghani

Publication date 24 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b99859

Mathematics Subject Classification ID

Intuitionistic mathematics (03F55) Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Containers: Constructing strictly positive types
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• scientific article; zbMATH DE number 1400097
• Wellfounded trees in categories
• Positive inductive-recursive definitions

Cited in

(13)

• Wellfounded trees in categories
• Deep induction: induction rules for (truly) nested types
• Containers: Constructing strictly positive types
• Continuous functions on final coalgebras
• Partiality, state and dependent types
• Polynomial functors and polynomial monads
• scientific article; zbMATH DE number 1400097 (Why is no real title available?)
• Multi-dimensional arrays with levels
• Is sized typing for Coq practical?
• Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
• Universal algebra in UniMath
• Distributive laws of monadic containers
• Formalising inductive and coinductive containers

This page was built for publication: Representing nested inductive types using W-types

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