Conference Proceeding

An Experiment using Term Rewriting Techniques for Concurrency


Shankland C (1991) An Experiment using Term Rewriting Techniques for Concurrency. In: Peyton JS, Hutton G & Holst C (eds.) Functional Programming, Glasgow 1990: Proceedings of the 1990 Glasgow Workshop on Functional Programming 13–15 August 1990, Ullapool, Scotland. Workshops in Computing. 1990 Glasgow Workshop on Functional Programming, Ullapool, UK, 13.08.1990-15.08.1990. London: Springer, pp. 196-200.;

The purpose of this extended abstract is to report on a preliminary investigation into the use of term rewriting theorem proving to support verification of formal description techniques for concurrent systems. The RRL [1, 2] system, particularly.Knuth-Bendix completion and equational proofs, is used to investigate verification of specifications written in the formal description language LOTOS. This work was completed as part of the SERC/IED ERIL project, which is investigating the use of Equational Reasoning for LOTOS. A more complete presentation of the results given here may be found in [3]. That paper also reports on complementary work, also undertaken as part of the ERIL project, using the LP theorem prover [4] for equational and inductive proofs about CSP [5].

Title of seriesWorkshops in Computing
Publication date31/12/1991
Publication date online31/08/1990
Publisher URL…-4471-3810-5_16#
Place of publicationLondon
ISSN of series1431-1682
Conference1990 Glasgow Workshop on Functional Programming
Conference locationUllapool, UK