Some Remarks on Type Systems for Course-of-value Recursion

DOI10.1016/j.entcs.2009.07.051zbMath1310.68055OpenAlexW2114009375MaRDI QIDQ5178964

Favio E. Miranda-Perea

Publication date: 18 March 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.07.051

zbMATH Keywords

category theory(co)inductive typestyped \(\lambda\)-calculusleast fixed pointshistomorphismcourse-of-valueschemes of (co)recursion

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)

Related Items

Getting There and Back Again ⋮ Selective Memoization with Box Types ⋮ Two extensions of system F with (co)iteration and primitive (co)recursion principles

Cites Work

• Iteration and coiteration schemes for higher-order and nested datatypes
• Recursion Schemes for Dynamic Programming
• Categories for Types
• Monotone (co)inductive types and positive fixed-point types
• Least and greatest fixed points in intuitionistic natural deduction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item