We study the relationship between the encodings of the #lambda#-calculus into #pi#-calculus, the Continuation Passing Style (CPS) transforms, and the compilation of the Higher-Order #pi#-calculus (HO#pi#) into #pi#-calculus. We factorise the #pi#-calculus encodings of (untyped as well as simply-typed) call-by-name and call-by-value #lambda#-calculus into three steps: a CPS transform, the inclusion of CPS terms into HO#pi# and the compilation from HO#pi# to #pi#-calculus. The factorisations are used both to derive the encodings and to prove their correctness.
展开▼
