Logic in Computer Science (LICS 1997)

Paper: Unique Fixpoint Induction for Value-Passing Processes (at LICS 1997)

Authors: Julian Rathke

Abstract

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}
  }