Paper: Unique Fixpoint Induction for Value-Passing Processes (at LICS 1997)
Authors: Julian RathkeAbstract
We investigate the use of unique fixpoint induction as a proof method for value-passing process languages with recursion. An intuitive generalization of unique fixpoint induction based on loop invariants for symbolic graphs yields strong completeness results; we give an axiomatic characterization of both late and early observational congruence for a class of fully parameterised processes. This new, generalised, rule is shown to be derivable from existing formulations of unique fixpoint induction for value-passing calculi, thereby providing original completeness results. An example of the use of this new rule is presented in detail.
BibTeX
@InProceedings{Rathke-UniqueFixpointInduc, author = {Julian Rathke}, title = {Unique Fixpoint Induction for Value-Passing Processes}, booktitle = {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997}, year = 1997, editor = {Glynn Winskel}, month = {June}, pages = {140--148}, location = {Warsaw, Poland}, publisher = {IEEE Computer Society Press} }