Concurrent Logical Framework II: Examples and Applications

摘要

CLF is a new logical framework with an intrinsic notion of concurrency. It is designed as a conservative extension of the linear logical framework LLF with the synchronous connectives (circle multiply, 1, and there exists) of intuitionistic linear logic, encapsulated in a monad. LLF is itself a conservative extension of LF with the asynchronous connectives (logical negation, and T). In this report, the second of two technical reports describing CLF, we illustrate the expressive power of the framework by encoding several different concurrent languages including both the synchronous and asynchronous pi-calculus, an ML-like language with futures, lazy evaluation and concurrency primitives in the style of CML, Petri nets and finally, the security protocol specification language MSR. Throughout the report we assume the reader is already familiar with the formal definition of CLF. For detailed explanation and development of the type theory, please see A Concurrent Logical Framework I: Judgments and Properties WCPW02.