Specifying Properties of Concurrent Computations in CLF

CLF (the Concurrent Logical Framework) is a language for specifying and reasoning about concurrent systems. Its most significant feature is the first-class representation of concurrent executions as monadic expressions. We illustrate the representation techniques available within CLF by applying them to an asynchronous pi-calculus with correspondence assertions, including its dynamic semantics, safety criterion, and a type system with latent effects due to Gordon and Jeffrey. Key words: logical frameworks, type theory, linear logic, concurrency

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker
• Keywords: Concurrent Executions, Concurrent Logical Framework, ENTCS 2008, Logical Frameworks