Encoding call-by-push-value in the pi-calculus
Authors
Steffensen, Peter Buus ; Bennetzen, Benjamin Clausen ; Kristensen, Nikolaj Rossander
Term
4. term
Education
Publication year
2025
Submitted on
2025-06-05
Pages
56
Abstract
This thesis builds a bridge between a core model of programming languages and a core model of communicating processes. We define a translation (encoding) from Levy’s call-by-push-value lambda calculus (CBPV), which cleanly separates values from computations, into the pi-calculus, a formal model for concurrent message passing. We prove that the translation is sound and complete: it preserves and reflects program behavior, so equivalent CBPV programs translate to behaviorally equivalent pi-processes, and vice versa. To simplify reasoning and make it amenable to machine checking, we specialize the translation to the internal pi-calculus. In this setting, several variants of bisimulation (a standard test for behavioral equivalence) coincide, and bisimulation is a congruence, enabling modular proofs. This choice also helps avoid technical hurdles with de Bruijn indices in a formalization. We provide informal, by-hand proofs of soundness, completeness, and the supporting lemmas. We also argue that the encoding satisfies Gorla’s five established criteria for good encodings. In addition, we highlight similarities with Milner’s classic encodings of call-by-value and call-by-name into the pi-calculus. Beyond the internal calculus, we present CBPV encodings targeting the asynchronous polyadic and the local variants of the pi-calculus. Finally, we begin a Coq formalization of the soundness and completeness results for the internal pi-calculus case. Not all auxiliary lemmas are yet mechanized, but we justify them by hand proofs or by routine proof-assistant steps that follow from the informal arguments.
I dette speciale bygger vi en bro mellem en grundmodel for programmeringssprog og en grundmodel for kommunikerende processer. Vi definerer en oversættelse (kodning) fra Levys call-by-push-value lambda-kalkyle (CBPV), som skelner skarpt mellem værdier og beregninger, til pi-kalkylen, en formel model for samtidige systemer med meddelelsesudveksling. Vi viser, at oversættelsen er både lydhed og fuldstændighed: den bevarer og afspejler programadfærd, så ækvivalente CBPV-programmer bliver til adfærdsmæssigt ækvivalente pi-processer og omvendt. For at forenkle ræsonnementet og gøre det velegnet til maskinel verifikation specialiserer vi oversættelsen til den interne pi-kalkyle. Her falder flere varianter af bisimulation (en standardmetode til at teste adfærdsmæssig ækvivalens) sammen, og bisimulation er en kongruens, hvilket giver modulære beviser. Valget hjælper også med at undgå tekniske udfordringer med de Bruijn-indekser i en formalisering. Vi giver uformelle, håndskrevne beviser for lydhed, fuldstændighed og de nødvendige lemmaer. Vi argumenterer desuden for, at kodningen opfylder Gorlas fem anerkendte kriterier for gode kodninger. Derudover peger vi på ligheder med Milners klassiske kodninger af call-by-value og call-by-name i pi-kalkylen. Ud over den interne kalkyle præsenterer vi CBPV-kodninger til den asynkrone polyadiske og den lokale variant af pi-kalkylen. Endelig påbegynder vi en Coq-formalisering af lydheds- og fuldstændighedsresultaterne for den interne pi-kalkyle. Ikke alle hjælpelemmaer er endnu formaliseret, men vi begrunder dem ved håndbeviser eller rutinemæssige skridt i bevisassistenten, der følger af de uformelle argumenter.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords