Specifying Properties of Concurrent Computations in CLF

Kevin Watkins; Iliano Cervesato; Frank Pfenning; David Walker

doi:10.1016/j.entcs.2007.11.013

Specifying Properties of Concurrent Computations in CLF

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Computer Science

Research output: Contribution to journal › Article › peer-review

15 Scopus citations

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	https://doi.org/10.1016/j.entcs.2007.11.013
State	Published - Feb 24 2008

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Keywords

concurrency
linear logic
logical frameworks
type theory

Access to Document

10.1016/j.entcs.2007.11.013

Cite this

@article{5e406f6cd8954b139855f9aee30ed520,

title = "Specifying Properties of Concurrent Computations in CLF",

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.",

keywords = "concurrency, linear logic, logical frameworks, type theory",

author = "Kevin Watkins and Iliano Cervesato and Frank Pfenning and David Walker",

note = "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: kw@cs.cmu.edu 2 Email: iliano@cmu.edu 3 Email: fp@cs.cmu.edu 4 Email: dpw@cs.princeton.edu",

year = "2008",

month = feb,

day = "24",

doi = "10.1016/j.entcs.2007.11.013",

language = "English (US)",

volume = "199",

pages = "67--87",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

}

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: kw@cs.cmu.edu 2 Email: iliano@cmu.edu 3 Email: fp@cs.cmu.edu 4 Email: dpw@cs.princeton.edu

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 -

Specifying Properties of Concurrent Computations in CLF

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this