A master thesis from Aalborg University
Encoding call-by-push-value in the pi-calculus
Term
4. term
Education
Publication year
2025
Submitted on
2025-06-05
Pages
56 pages
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
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.