TY - JOUR
T1 - Specifying Properties of Concurrent Computations in CLF
AU - Watkins, Kevin
AU - Cervesato, Iliano
AU - Pfenning, Frank
AU - Walker, David
N1 - Funding Information:
★ This research was sponsored in part by the NSF under grants CCR-9988281, CCR-0208601, CCR-0238328, and CCR-0306313, and by NRL under grant N00173-00-C-2086. 1 Email: [email protected] 2 Email: [email protected] 3 Email: [email protected] 4 Email: [email protected]
PY - 2008/2/24
Y1 - 2008/2/24
N2 - 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.
AB - 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.
KW - concurrency
KW - linear logic
KW - logical frameworks
KW - type theory
UR - http://www.scopus.com/inward/record.url?scp=44449127078&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=44449127078&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2007.11.013
DO - 10.1016/j.entcs.2007.11.013
M3 - Article
AN - SCOPUS:44449127078
SN - 1571-0661
VL - 199
SP - 67
EP - 87
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -