Milner encodings

Milner encodings are a class of language translations from functional programming languages (such as the \lambda-calculus) to concurrent, message passing calculi (such as the \pi-calculus).

The original encodings by Robin Milner translated the (untyped) lazy \lambda-calculus to a fragment of the untyped \pi-calculus, in both CBN and CBV variants.

Soundness

Most Milner encodings are constructed so as to be sound for an equational theory \mathcal{T}, in the sense that equality in the theory \mathcal{T} should imply (some form of) behavioural equivalence in the target calculus:

	\mathcal{T} \vdash M = N \quad\Longrightarrow\quad \llbracket M \rrbracket \sim \llbracket N \rrbracket

References

• Milner encodings were introduced in

@article{milner_1992,
	title = {Functions as processes},
	volume = {2},
	doi = {10.1017/S0960129500001407},
	number = {2},
	journal = {Mathematical Structures in Computer Science},
	author = {Milner, Robin},
	year = {1992},
	pages = {119--141}
}