Encoding call-by-push-value in the pi-calculus

TL;DR

This paper presents a formal encoding of call-by-push-value lambda-calculus into the pi-calculus, demonstrating soundness, completeness, and satisfying criteria for good encodings, with formalization efforts in Coq.

Contribution

It introduces a novel encoding of CBPV into pi-calculus that is sound, complete, and aligns with Gorla's criteria, including formalization in Coq.

Findings

Encoding is sound and complete.

Bisimulation properties are simplified in the specialized setting.

Encoding satisfies Gorla's criteria for good encodings.

Abstract

In this report we define an encoding of Levys 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 (pi-i-calculus) to circumvent certain challenges associated with using de Bruijn index 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 Milners and our encoding. This paper includes encodings from CBPV in the pi-i-calculus, asynchronous polyadic pi-calculus and the local pi-calculus. We begin a formalization of the proof in Coq for the soundness and completeness of the encoding in the pi-i-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.