Leaf-First Zipper Semantics

Biernacka et al. recently proposed zipper semantics, a semantics format from which sound and complete abstract machines for non-deterministic languages can be automatically derived. We present a new style of zipper semantics, called leaf-first, in which we express the semantics of two extensions of HO \(\pi \) , a higher-order version of the \(\pi \) -calculus: one with passivation and the other with join patterns. The leaf-first style is better suited than the original one to express phenomena occurring in process calculi semantics such as scope extrusion, which is observable with passivation and complex with join patterns.