We study Milner's lambda-calculus with partial substitutions. Particularly, we show confluence on terms and metaterms, preservation of \b{eta}-strong normalisation and characterisation of strongly normalisable terms via an intersection typing discipline. The results on terms transfer to Milner's bigraphical model of the calculus. We relate Milner's calculus to calculi with definitions, to calculi with explicit substitutions, and to MELL Proof-Nets.

翻译：我们研究了Milner的带部分替换的λ-演算。具体而言，我们展示了项与元项上的合流性、\b{eta}-强规范化的保持性，以及通过交集类型系统对强规范化项的特征刻画。关于项的结果可迁移至Milner的双图模型。我们将Milner的演算与带定义演算、显式替换演算以及MELL证明网进行了关联。