Automating algebraic reasoning for CSP processes
Supervisors
Suitable for
Abstract
It is often useful to rewrite a CSP process into a sequential form, using a combination of algebraic laws, particularly step laws, and the Unique Fixed Point rule. Many exercises on the Concurrency course ask students to perform such rewriting. The aim of this project is to automate this rewriting. It is hoped that the resulting processes will be easier to understand. Also, the tool should be useful pedagogically. The project will build on the Haskell CSP evaluator [1].This project would require the Concurrency course and experience of programming in Haskell.
[1] libcspm: https://github.com/tomgr/libcspm