A Concurrent Logical Framework II: Examples and Applications
Iliano Cervesato, Frank Pfenning, David P. Walker, Kevin Watkins · 2003
CLF is a new logical framework with an intrinsic notion of concurrency.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 π-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].