Matching is an important component of a logical framework. It is at the heart of many reasoning tasks and is sufficient to support the operational semantic of well-moded logic programs. Matching is poorly understood for logical frameworks such as CLF, designed to effectively capture the specifications of parallel, concurrent and distributed systems. The witnesses of their computations, and therefore their term language, are concurrent traces. A concurrent trace is a sequence of computations where independent steps can be permuted. We study the problems of matching concurrent traces on large fragments of CLF. Specifically, we give a sound and complete algorithm for matching traces with a single variable standing for an unknown subtrace. We also examine the unification problem for some simple fragments of CLF and give an algorithm for solving unification problems with with one variable standing for an unknown subtrace on each side of the equation.

65 pages

*Computer Science Department, Carnegie Mellon University, Pittsburgh
**IT University of Copenhagen, Denmark

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu