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.
Original language | English (US) |
---|---|
Pages (from-to) | 67-87 |
Number of pages | 21 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 199 |
DOIs | |
State | Published - Feb 24 2008 |
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- General Computer Science
Keywords
- concurrency
- linear logic
- logical frameworks
- type theory