Tools
Rathke, Julian (1997) Unique fixpoint induction for value-passing processes. In: Unset, Proceedings of the 12th Annual Symposium of Logic in Computer Science Warsaw. IEEE Computer Society Press..
Full text not available from this repository.
Official URL: http://www.sciencedirect.com/science/article/pii/S...
Abstract
We present a proof system for message-passing process calculi with recursion. The key inference rule to deal with recursive processes is a version of Unique Fixpoint Induction for process abstractions. We prove that the proof system is sound and also complete for guarded regular message-passing processes. We also show that the system is incomplete for unguarded processes and discuss more powerful extensions with inductive inference rules.
Item Type: | Conference or Workshop Item (Paper) |
---|---|
Schools and Departments: | School of Engineering and Informatics > Informatics |
Depositing User: | EPrints Services |
Date Deposited: | 06 Feb 2012 18:52 |
Last Modified: | 31 May 2012 13:29 |
URI: | http://sro.sussex.ac.uk/id/eprint/18720 |