A direct proof of the finite developments theorem

DOI10.2307/2274219MaRDI QIDQ3735687zbMATH OpenOpenAlexFDO

Authors Roel de Vrijer

Publication date 1985

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2307/2274219

zbMATH Keywords

lambda calculusWeak Combinatory Logic

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 806614
• Generalized finite developments
• scientific article; zbMATH DE number 992007
• scientific article; zbMATH DE number 4045707
• A direct proof of the confluence of combinatory strong reduction

Cited in

(11)

• scientific article; zbMATH DE number 5056505 (Why is no real title available?)
• A Note on Shortest Developments
• Effective longest and infinite reduction paths in untyped λ-calculi
• Least upper bounds on the size of Church-Rosser diagrams in term rewriting and -calculus
• Perpetual reductions in -calculus
• On the longest perpetual reductions in orthogonal expression reduction systems
• Generalized finite developments
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• One is all you need: associative second-order unification without first-order variables
• On strong normalization and type inference in the intersection type discipline
• Descendants and origins in term rewriting.

This page was built for publication: A direct proof of the finite developments theorem

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