A coinductive confluence proof for infinitary lambda-calculus

DOI10.1007/978-3-319-08918-8_12MaRDI QIDQ5170815zbMATH OpenOpenAlexFDO

Authors Łukasz Czajka

Publication date 24 July 2014

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

Full work available at URL https://doi.org/10.1007/978-3-319-08918-8_12

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Recommendations

• Confluence of the coinductive \(\lambda\)-calculus
• scientific article; zbMATH DE number 6678680
• On Confluence of Infinitary Combinatory Reduction Systems
• Applications of infinitary lambda calculus
• Böhm Reduction in Infinitary Term Graph Rewriting Systems

Cited in

(9)

• Constructive proofs of the range property in lambda calculus
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• scientific article; zbMATH DE number 1722714 (Why is no real title available?)
• An Alpha-Corecursion Principle for the Infinitary Lambda Calculus
• Coinductive foundations of infinitary rewriting and infinitary equational logic
• Sequence types for hereditary permutators
• A new coinductive confluence proof for infinitary lambda calculus
• scientific article; zbMATH DE number 7168147 (Why is no real title available?)
• Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications

This page was built for publication: A coinductive confluence proof for infinitary lambda-calculus

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