A term calculus for (co-)recursive definitions on streamlike data structures

DOI10.1016/J.APAL.2005.05.006MaRDI QIDQ2566066zbMATH OpenOpenAlexFDO

Authors Wilfried Buchholz

Publication date 22 September 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2005.05.006

zbMATH Keywords

(co-)recursion equationscontinuous cut-eliminationsimply typed lambda terms

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40) Abstract data types; algebraic specification (68Q65)

Recommendations

• Concrete stream calculus: an extended study
• A coinductive calculus of streams
• Partial inductive definitions as type-systems for \(\lambda\)-terms
• Elements of stream calculus (an extensive exercise in coinduction)
• Typed λ-calculus with recursive definitions

Cites work

• scientific article; zbMATH DE number 107999 (Why is no real title available?)
• scientific article; zbMATH DE number 2003155 (Why is no real title available?)
• scientific article; zbMATH DE number 1424015 (Why is no real title available?)
• Finite investigations of transfinite derivations

Cited in

(14)

• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• Using Structural Recursion for Corecursion
• Lazy productivity via termination
• Coinduction for exact real number computation
• Productivity of stream definitions
• The $\Pi^0_2$ -Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity)
• Pure type systems with corecursion on streams, from finite to infinitary normalisation
• A user's friendly syntax to define recursive functions as typed λ-terms
• Upper Bounds on Stream I/O Using Semantic Interpretations
• Concrete stream calculus: an extended study
• Structured general corecursion and coinductive graphs (extended abstract)
• Inductive and coinductive components of corecursive functions in Coq
• Functional pearl: streams and unique fixed points
• scientific article; zbMATH DE number 3903936 (Why is no real title available?)

This page was built for publication: A term calculus for (co-)recursive definitions on streamlike data structures

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