Loading...
Please wait, while we are loading the content...
Similar Documents
Trace matching in a concurrent logical framework
| Content Provider | ACM Digital Library |
|---|---|
| Author | Simmons, Robert J. Cervesato, Iliano Schürmann, Carsten Pfenning, Frank Sacchini, Jorge Luis |
| Abstract | 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. |
| Starting Page | 1 |
| Ending Page | 12 |
| Page Count | 12 |
| File Format | |
| ISBN | 9781450315784 |
| DOI | 10.1145/2364406.2364408 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2012-09-09 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Matching Logical frameworks Concurrent traces |
| Content Type | Text |
| Resource Type | Article |
