The Structural lambda -Calculus

Abstract Inspired by a recent graphical formalism for λ -calculus based on Linear Logic technology, we introduce an untyped structural λ -calculus, called λj, which combines action at a distance with exponential rules decomposing the substitution by means of weakening, contraction and dereliction. Firstly, we prove fundamental properties such as confluence and preservation of β -strong normalisation. Secondly, we use λj to describe known notions of developments and superdevelopments, and introduce a more general one called XL -development. Then we show how to reformulate Regnier’s σ -equivalence in λj so that it becomes a strong bisimulation. Finally, we prove that explicit composition or de-composition of substitutions can be added to λj while still preserving β -strong normalisation.

Authors

• Beniamino Accattoli
• Delia Kesner

Keywords

No keywords are indexed for this paper.