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

DOI10.1016/J.JLAP.2004.01.008zbMath1090.68019OpenAlexW2082949147MaRDI QIDQ1763159

Roel Bloo, Fairouz Kamareddine

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.008

zbMATH Keywords

Strong normalisationType theoryClass reductionSubject reduction

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (1)

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

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• CPS transformation of beta-redexes
• On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations
• An equivalence between lambda- terms
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• A useful \(\lambda\)-notation
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
• An analysis of ML typability
• Postponement, conservation and preservation of strong normalization for generalized reduction

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