Milner encodings are a class of language translations from functional programming languages (such as the -calculus) to concurrent, message passing calculi (such as the -calculus).
The original encodings by Robin Milner translated the (untyped) lazy -calculus to a fragment of the untyped -calculus, in both CBN and CBV variants.
Most Milner encodings are constructed so as to be sound for an equational theory , in the sense that equality in the theory should imply (some form of) behavioural equivalence in the target calculus:
Milner, Robin. 1992. ‘Functions as Processes’. Mathematical Structures in Computer Science 2 (2): 119–41. https://doi.org/10.1017/S0960129500001407.
@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}
}