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

DOI10.1051/ITA/2009015MaRDI QIDQ3653093zbMATH OpenOpenAlexFDO

Authors 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

coalgebrascoiterationcorecursiondialgebrasiterationmonotone coinductive typemonotone inductive typemonotonicity witnessprimitive recursionsaturated setsSystem F

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1385477
• scientific article; zbMATH DE number 1956505
• Monotone (co)inductive types and positive fixed-point types
• Iteration and coiteration schemes for higher-order and nested datatypes
• Inductive, coinductive, and pointed types

Cites work

• Automatic synthesis of typed -programs on term algebras
• Categories for Types
• Category theory and computer science. Manchester, UK, September 5--8, 1989. Proceedings
• Comparing Hagino's categorical programming language and typed lambda- calculi
• From algebras and coalgebras to dialgebras
• scientific article; zbMATH DE number 4047683 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 3513750 (Why is no real title available?)
• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• scientific article; zbMATH DE number 1304993 (Why is no real title available?)
• scientific article; zbMATH DE number 1342219 (Why is no real title available?)
• scientific article; zbMATH DE number 1343506 (Why is no real title available?)
• scientific article; zbMATH DE number 1064116 (Why is no real title available?)
• scientific article; zbMATH DE number 1552770 (Why is no real title available?)
• scientific article; zbMATH DE number 1748069 (Why is no real title available?)
• scientific article; zbMATH DE number 1841846 (Why is no real title available?)
• scientific article; zbMATH DE number 3348059 (Why is no real title available?)
• Inductive types and type constraints in the second-order lambda calculus
• Iteration and coiteration schemes for higher-order and nested datatypes
• Least and greatest fixed points in intuitionistic natural deduction
• Monotone (co)inductive types and positive fixed-point types
• Non-strictly positive fixed points for classical natural deduction
• Recursion Schemes for Dynamic Programming
• Recursive programming with proofs
• Some remarks on type systems for course-of-value recursion
• The under-appreciated unfold
• Type fixpoints, iteration vs. recursion

Cited in

(5)

• Iteration and coiteration schemes for higher-order and nested datatypes
• Inductive, coinductive, and pointed types
• Algebras and coalgebras in the light affine lambda calculus
• scientific article; zbMATH DE number 1385477 (Why is no real title available?)
• Some remarks on type systems for course-of-value recursion

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

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