COMPUTER SCIENCE QATAR TECHNICAL REPORT ABSTRACTS

Source: http://reports-archive.adm.cs.cmu.edu/anon/qatar/abstracts/12-114.html Parent: http://reports-archive.adm.cs.cmu.edu/qatar.html


	CMU-CS-QTR-114 Computer Science Qatar School of Computer Science, Carnegie Mellon University --- CMU-CS-QTR-114 On Matching in CLF Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann, Robert J. Simmons July 2012 CMU-CS-QTR-114.pdf Also appears as Computer Science Department Technical Report CMU-CS-12-114 Keywords: CLF, concurrent traces, matching, unification, reasoning about concurrency 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

CMU-CS-QTR-114 Computer Science Qatar School of Computer Science, Carnegie Mellon University --- CMU-CS-QTR-114 On Matching in CLF Iliano Cervesato, Frank Pfenning*, Jorge Luis Sacchini, Carsten Schürmann**, Robert J. Simmons* July 2012 CMU-CS-QTR-114.pdf Also appears as Computer Science Department Technical Report CMU-CS-12-114 Keywords: CLF, concurrent traces, matching, unification, reasoning about concurrency 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