Upper bounds for standardizations and an application

DOI10.2307/2586765zbMath0938.03027OpenAlexW2132042970MaRDI QIDQ4254636

Hongwei Xi

Publication date: 22 June 2000

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

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

zbMATH Keywords

\(\lambda\)-calculussimply typed \(\lambda\)-calculus\(\beta\)-reduction sequencestandarization theorem

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (5)

Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters ⋮ Chemical Term Reduction with Active P Systems ⋮ Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus ⋮ An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus ⋮ Exact bounds for acyclic higher-order recursion schemes

Cites Work

• Unnamed Item
• The typed lambda-calculus is not elementary recursive
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• The Standardization Theorem for λ‐Calculus
• Ordinal analysis of terms of finite type
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Residual theory in λ-calculus: a formal development
• Resolution in type theory
• Parallel reductions in \(\lambda\)-calculus

This page was built for publication: Upper bounds for standardizations and an application