An equivalence between lambda- terms

DOI10.1016/0304-3975(94)90012-4zbMath0801.03013OpenAlexW2008868842MaRDI QIDQ1322165

Laurent Regnier

Publication date: 9 June 1994

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90012-4

zbMATH Keywords

lambda calculusoperational properties of lambda-termsperpetual strategysigma- equivalence

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (30)

Unnamed Item ⋮ Open Call-by-Value ⋮ Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Resource operators for \(\lambda\)-calculus ⋮ Extensional proofs in a propositional logic modulo isomorphisms ⋮ Proof nets and the call-by-value \(\lambda\)-calculus ⋮ A faithful and quantitative notion of distant reduction for generalized applications ⋮ A short proof that adding some permutation rules to \(\beta \) preserves SN ⋮ A note on preservation of strong normalisation in the \(\lambda \)-calculus ⋮ Unnamed Item ⋮ Head reduction and normalization in a call-by-value lambda-calculus ⋮ Unnamed Item ⋮ Strong normalization through intersection types and memory ⋮ Intuitionistic differential nets and lambda-calculus ⋮ De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case ⋮ De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case ⋮ Evaluating lambda terms with traversals ⋮ Unnamed Item ⋮ An exact correspondence between a typed pi-calculus and polarised proof-nets ⋮ The bang calculus revisited ⋮ On the longest perpetual reductions in orthogonal expression reduction systems ⋮ Classical By-Need ⋮ The bang calculus revisited ⋮ An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form ⋮ Monadic Translation of Intuitionistic Sequent Calculus ⋮ Intersection Types for the Resource Control Lambda Calculi ⋮ Perpetual reductions in \(\lambda\)-calculus ⋮ Polarized proof-nets and \(\lambda \mu\)-calculus ⋮ Effective longest and infinite reduction paths in untyped λ-calculi

Cites Work

• Linear logic
• Unnamed Item
• Unnamed Item

This page was built for publication: An equivalence between lambda- terms