An equivalence between lambda- terms

DOI10.1016/0304-3975(94)90012-4MaRDI QIDQ1322165zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 627411
• The permutative \(\lambda \)-calculus
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
• scientific article; zbMATH DE number 1088031
• Four equivalent equivalences of reductions

Cites work

• scientific article; zbMATH DE number 3875232 (Why is no real title available?)
• scientific article; zbMATH DE number 46869 (Why is no real title available?)
• Linear logic

Cited in

(36)

• An exact correspondence between a typed pi-calculus and polarised proof-nets
• A strong bisimulation for a classical term calculus
• scientific article; zbMATH DE number 7526055 (Why is no real title available?)
• scientific article; zbMATH DE number 1231514 (Why is no real title available?)
• An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
• Effective longest and infinite reduction paths in untyped λ-calculi
• The permutative \(\lambda \)-calculus
• Strong normalization through intersection types and memory
• Evaluating lambda terms with traversals
• Intuitionistic differential nets and lambda-calculus
• Classical by-need
• Monadic Translation of Intuitionistic Sequent Calculus
• Extensional proofs in a propositional logic modulo isomorphisms
• A note on discriminability of lambda terms
• Polarized proof-nets and \(\lambda \mu\)-calculus
• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
• Perpetual reductions in -calculus
• A notation for lambda terms. A generalization of environments
• Intersection types for the resource control lambda calculi
• On the longest perpetual reductions in orthogonal expression reduction systems
• A faithful and quantitative notion of distant reduction for generalized applications
• Open call-by-value
• 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
• The bang calculus revisited
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Proof nets and the call-by-value \(\lambda\)-calculus
• scientific article; zbMATH DE number 7226008 (Why is no real title available?)
• A note on preservation of strong normalisation in the \(\lambda \)-calculus
• A short proof that adding some permutation rules to \(\beta \) preserves SN
• The bang calculus revisited
• Resource operators for \(\lambda\)-calculus
• Linear \(\beta\)-reduction
• A resource aware semantics for a focused intuitionistic calculus
• Head reduction and normalization in a call-by-value lambda-calculus
• scientific article; zbMATH DE number 4179330 (Why is no real title available?)

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1322165)