Specifying Properties of Concurrent Computations in CLF

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Research output: Contribution to journalArticle

16 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 languageEnglish (US)
Pages (from-to)67-87
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Volume199
DOIs
StatePublished - Feb 24 2008

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Keywords

  • concurrency
  • linear logic
  • logical frameworks
  • type theory

Fingerprint Dive into the research topics of 'Specifying Properties of Concurrent Computations in CLF'. Together they form a unique fingerprint.

  • Cite this