A concurrent logical framework: The propositional fragment

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Research output: Chapter in Book/Report/Conference proceedingChapter

41 Scopus citations

Abstract

We present the prepositional fragment CLFo of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations in an object language. The underlying type theory uses monadic types to segregate values from computations. This separation leads to a tractable notion of definitional equality that identifies computations differing only in the order of execution of independent steps. From a logical point of view our type theory can be seen as a novel combination of lax logic and dual intuitionistic linear logic. An encoding of a small Petri net exemplifies the representation methodology, which can be summarized as "concurrent computations as monadic expressions".

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsStefano Berardi, Mario Coppo, Ferruccio Damiani
PublisherSpringer Verlag
Pages355-377
Number of pages23
ISBN (Print)3540221646
DOIs
StatePublished - Jan 1 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3085
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A concurrent logical framework: The propositional fragment'. Together they form a unique fingerprint.

  • Cite this

    Watkins, K., Cervesato, I., Pfenning, F., & Walker, D. (2004). A concurrent logical framework: The propositional fragment. In S. Berardi, M. Coppo, & F. Damiani (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 355-377). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3085). Springer Verlag. https://doi.org/10.1007/978-3-540-24849-1_23