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.
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Perera, Roly; Cheney, James: Proof-relevant (\pi)-calculus: a constructive account of concurrency and causality (2018)
- Watkins, Kevin; Cervesato, Iliano; Pfenning, Frank; Walker, David: Specifying properties of concurrent computations in CLF (2007)