Two extensions of system F with (co)iteration and primitive (co)recursion principles

DOI10.1051/ita/2009015zbMath1197.03013OpenAlexW2112269051MaRDI QIDQ3653093

Favio E. Miranda-Perea

Publication date: 18 December 2009

Published in: RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL: https://eudml.org/doc/92934

zbMATH Keywords

iterationcoalgebrasprimitive recursioncorecursionsaturated setsSystem Fdialgebrascoiterationmonotone coinductive typemonotone inductive typemonotonicity witness

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Cites Work

• Comparing Hagino's categorical programming language and typed lambda- calculi
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• Recursive programming with proofs
• Iteration and coiteration schemes for higher-order and nested datatypes
• Non-strictly positive fixed points for classical natural deduction
• Category theory and computer science. Manchester, UK, September 5--8, 1989. Proceedings
• Inductive types and type constraints in the second-order lambda calculus
• Type fixpoints
• Recursion Schemes for Dynamic Programming
• Categories for Types
• From Algebras and Coalgebras to Dialgebras
• Monotone (co)inductive types and positive fixed-point types
• Some Remarks on Type Systems for Course-of-value Recursion
• The under-appreciated unfold
• Least and greatest fixed points in intuitionistic natural deduction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Two extensions of system F with (co)iteration and primitive (co)recursion principles