An upper bound for reduction sequences in the typed \(\lambda\)-calculus

DOI10.1007/BF01621476zbMath0719.03007OpenAlexW2023773759MaRDI QIDQ2639840

Helmut Schwichtenberg

Publication date: 1991

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01621476

zbMATH Keywords

boundstyped lambda calculusreduction sequences

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (10)

Upper bounds for standardizations and an application ⋮ Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ A decidable theory of type assignment ⋮ Elementary Proof of Strong Normalization for Atomic F ⋮ Decidability of bounded higher-order unification ⋮ Exact bounds for lengths of reductions in typed λ-calculus ⋮ Extracting Herbrand disjunctions by functional interpretation ⋮ Perpetual reductions in \(\lambda\)-calculus ⋮ Exact bounds for acyclic higher-order recursion schemes ⋮ Effective longest and infinite reduction paths in untyped λ-calculi

Cites Work

• Unnamed Item
• Functionals defined by recursion
• Ordinal analysis of terms of finite type

This page was built for publication: An upper bound for reduction sequences in the typed \(\lambda\)-calculus