De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case

DOI10.1016/J.JLAP.2004.01.001zbMath1101.68452OpenAlexW4210256011MaRDI QIDQ1764799

Fairouz Kamareddine, Roel Bloo

Publication date: 22 February 2005

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2004.01.001

zbMATH Keywords

Canonical formsClass reductionReductional behaviour

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (1)

De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• CPS transformation of beta-redexes
• An equivalence between lambda- terms
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• A useful \(\lambda\)-notation
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case
• Principality and type inference for intersection types using expansion variables
• An analysis of ML typability
• Postponement, conservation and preservation of strong normalization for generalized reduction
• Refining reduction in the lambda calculus

This page was built for publication: De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case