Trace matching in a concurrent logical framework
Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann, Robert J. Simmons · 2012
Matching and unification play an important role in implementations of proof assistants, logical frameworks, and logic programming languages. In particular, matching is at the heart of many reasoning tasks and underlies the operational semantic for well-moded logic programs. In this paper, we study the problem of matching on concurrent traces in the CLF logical framework, an extension of LF that supports the specification of concurrent and distributed systems. A concurrent trace is a sequence of computations where independent steps can be permuted. We give a sound and complete algorithm for matching traces with one variable standing for an unknown subtrace. Extending the result to general traces and to unification is left to future work.