Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
422235 | Electronic Notes in Theoretical Computer Science | 2008 | 21 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics