TY - GEN
T1 - The structural λ-calculus
AU - Accattoli, Beniamino
AU - Kesner, Delia
PY - 2010/1/1
Y1 - 2010/1/1
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/77956599996
U2 - 10.1007/978-3-642-15205-4_30
DO - 10.1007/978-3-642-15205-4_30
M3 - Conference contribution
AN - SCOPUS:77956599996
SN - 364215204X
SN - 9783642152047
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 381
EP - 395
BT - Computer Science Logic - 24th International Workshop, CSL 2010, and 19th Annual Conference of the EACSL, Proceedings
PB - Springer Verlag
T2 - 24th International Workshop on Computer Science Logic, CSL 2010, and 19th Annual Conference of the EACSL
Y2 - 23 August 2010 through 27 August 2010
ER -