|
Abstract : |
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, 1,!, and of intuitionistic linear logic, encapsulated in a monad. LLF is itself a conservative extension of LF with the asynchronous connectives & and In this report, the second of two technical reports describing CLF, we illustrate the expressive power of the framework by encoding several di#erent concurrent languages including both the synchronous and asynchronous #-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, |
