Encoding call-by-push-value in the pi-calculus
Term
4. term
Education
Publication year
2025
Submitted on
2025-06-05
Pages
56
Abstract
In this report we define an encoding of Levy's call-by-push-value lambda-calculus (CBPV) in the pi-calculus, and prove that our encoding is both sound and complete. We present informal (by-hand) proofs of soundness, completeness, and all required lemmas. The encoding is specialized to the internal pi-calculus to circumvent certain challenges associated with using de Bruijn indices in a formalization, and it also helps with bisimulation as early-, late- and open-bisimulation coincide in this setting, furthermore bisimulation is a congruence. Additionally, we argue that our encoding also satisfies the five criteria for good encodings proposed by Gorla, as well as show similarities between Milner's original encodings of call-by-value and call-by-name in the pi-calculus and our encoding. This paper includes encodings from CBPV in the internal-, asynchronous polyadic- and the local pi-calculus. We begin a formalization of the proof in Coq for the soundness and completeness of the encoding in the internal pi-calculus. Not all lemmas used in the formalization are themselves formally proven. However, we argue that the non-proven lemmas are reasonable, as they are proven by hand, or amount to Coq formalities that are straightforward given informal arguments.
Keywords
Documents