Conservation and uniform normalization in lambda calculi with erasing reductions

DOI10.1016/S0890-5401(02)93153-6zbMath1012.03022MaRDI QIDQ1854562

Morten Heine B. Sørensen, Peter Møller Neergaard

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

03B40: Combinatory logic and lambda calculus

Related Items

Perpetuality and uniform normalization in orthogonal rewrite systems

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Semantical analysis of perpetual strategies in \(\lambda\)-calculus
• Perpetual reductions in \(\lambda\)-calculus
• The ant-lion paradigm for strong normalization
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Perpetuality and uniform normalization in orthogonal rewrite systems
• Intensional interpretations of functionals of finite type I
• Proving algorithms by tail functions
• Some Properties of Conversion
• Parallel reductions in \(\lambda\)-calculus
• Weak normalization implies strong normalization in a class of non-dependent pure type systems