A Current Logical Framework: The Propositional Fragment

Abstract

We present the propositional fragment CLF 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".

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2003
Accession Number
ADA418510

Entities

People

  • David Walker
  • Frank Pfenning
  • Iliano Cervesato
  • Kevin Watkins

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Algorithms
  • Calculus
  • Coding
  • Computations
  • Computer Programming
  • Computer Science
  • Elimination
  • Encapsulation
  • Equations
  • Identities
  • Judgment
  • Language
  • Multithreading
  • Notation
  • Petri Nets
  • Programming Languages
  • Standards

Readers

  • Artificial Intelligence
  • Mathematical Modeling and Probability Theory.
  • Systems Analysis and Design