A decompilation of the pi-calculus and its application to termination

2011/02/11 by Roberto M. Amadio, Roberto Amadio, Amadio, Roberto
Computer Science · #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.PL

paper · pdf · doi:10.48550/arxiv.1102.2339

arxiv created 2011/02/11 · arxiv updated 2011/02/14

Abstract

We study the correspondence between a concurrent lambda-calculus in administrative, continuation passing style and a pi-calculus and we derive a termination result for the latter.

Related

• Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination
• An Interactive Proof of Termination for a Concurrent λ-calculus with References and Explicit Substitutions
• Termination in Concurrency, Revisited
• Event structures for the reversible early internal Pi-calculus
• Encoding call-by-push-value in the pi-calculus