将CBPV语言编码到π演算中，证明其正确性并支持形式化验证。
Encoding call-by-push-value in the pi-calculus
- 用内部π演算实现CBPV的编码，避免变量绑定复杂性。
- 证明编码在语义上完全保持原语言的行为，且满足五项优秀编码标准。
- 适用于类型理论与形式化验证研究者，为程序语义建模提供新工具。
本文定义了莱维的调用推值（CBPV）λ演算在π演算中的编码，并证明该编码既正确又完整。通过手工证明了正确性、完备性及所有必要引理。编码针对内部π演算（pi-i-calculus）设计，以规避形式化中德布鲁因标记的挑战，并使早、晚和开式对等关系一致，且对等是同余关系。此外，论证该编码满足戈尔拉提出的五项优秀编码标准，并揭示其与米尔纳编码的相似性。论文还包含了在内部π演算、异步多参与π演算和局部π演算中的编码实现。目前正使用Coq对内部π演算中编码的正确性与完备性进行形式化，虽部分引理尚未正式证明，但认为其合理——因已由手工证明，或仅涉及可直接从非正式论证推出的Coq形式细节。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。