Session-based Type Discipline for Pi Calculus with Matching
Marco Giunti, Kohei Honda, VASCO THUDICHUM VASCONCELOS, Nobuko Yoshida · 2009
Introduction. In [7] we have introduced an extension of the first session typing system [10] that allows higherorder session communication. In the new system, the reduction rule for session passing k![k ′].P | k?(k ′).Q → P | Q does not allow the transmission of an arbitrary channel. In most situations a receiving process k?(k ′ ′).Q can be alpha-converted ahead of communication so that the bound channel k ′ ′ syntactically matches the free channel k ′