Document Open Access Logo

Structural Rewriting in the pi-Calculus

Author David Sabel

PDF

File

Thumbnail PDF
PDF
OASIcs.WPTE.2014.51.pdf
  • Filesize: 0.52 MB
  • 12 pages

Document Identifiers

Subject Classification

Keywords
  • Process calculi
  • Rewriting
  • Semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We consider reduction in the synchronous pi-calculus with replication, without sums. Usual definitions of reduction in the pi-calculus use a closure w.r.t. structural congruence
of processes. In this paper we operationalize structural congruence by providing a reduction relation for pi-processes which also performs necessary structural conversions explicitly by
rewrite rules. As we show, a subset of structural congruence axioms is sufficient. We show that our rewrite strategy is equivalent to the usual  strategy including structural congruence w.r.t.the observation of barbs and thus w.r.t. may- and should-testing equivalence in the pi-calculus.

Cite As Get BibTex

David Sabel. Structural Rewriting in the pi-Calculus. In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. 51-62, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/OASIcs.WPTE.2014.51

Author Details

David Sabel

References

  1. M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. In CCS'97, pages 36-47. ACM, 1997. Google Scholar
  2. J. Engelfriet and T. Gelsema. A new natural structural congruence in the pi-calculus with replication. Acta Inf., 40(6-7):385-430, 2004. Google Scholar
  3. J. Engelfriet and T. Gelsema. An exercise in structural congruence. Inf. Process. Lett., 101(1):1-5, 2007. Google Scholar
  4. C. Fournet and G. Gonthier. A hierarchy of equivalences for asynchronous calculi. J. Log. Algebr. Program., 63(1):131-173, 2005. Google Scholar
  5. J. Giesl, P. Schneider-Kamp, and R. Thiemann. Automatic termination proofs in the dependency pair framework. In IJCAR'06, volume 4130 of LNCS, pages 281-286. Springer, 2006. Google Scholar
  6. V. Khomenko and R. Meyer. Checking pi-calculus structural congruence is graph isomorphism complete. In ACSD'09, pages 70-79. IEEE, 2009. Google Scholar
  7. C. Laneve. On testing equivalence: May and must testing in the join-calculus. Technical Report UBLCS 96-04, University of Bologna, 1996. Google Scholar
  8. R. Milner. Communicating and Mobile Systems: the π-calculus. CUP, 1999. Google Scholar
  9. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, i &ii. Inform. and Comput., 100(1):1-77, 1992. Google Scholar
  10. J. H. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, MIT, 1968. Google Scholar
  11. V. Natarajan and R. Cleaveland. Divergence and fair testing. In ICALP'95, volume 944 of LNCS, pages 648-659. Springer, 1995. Google Scholar
  12. J. Niehren, D. Sabel, M. Schmidt-Schauß, and J. Schwinghammer. Observational semantics for a concurrent lambda calculus with reference cells and futures. Electron. Notes Theor. Comput. Sci., 173:313-337, 2007. Google Scholar
  13. G. D. Plotkin. Call-by-name, call-by-value, and the lambda-calculus. Theoret. Comput. Sci., 1:125-159, 1975. Google Scholar
  14. C. Priami. Stochastic pi-calculus. Comput. J., 38(7):578-589, 1995. Google Scholar
  15. C. Rau, D. Sabel, and M. Schmidt-Schauß. Correctness of program transformations as a termination problem. In IJCAR'12, volume 7364 of LNCS, pages 462-476. Springer, 2012. Google Scholar
  16. A. Rensink and W. Vogler. Fair testing. Inform. and Comput., 205(2):125-198, 2007. Google Scholar
  17. D. Sabel and M. Schmidt-Schauß. A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Math. Structures Comput. Sci., 18(03):501-553, 2008. Google Scholar
  18. D. Sabel and M. Schmidt-Schauß. A contextual semantics for Concurrent Haskell with futures. In PPDP'11, pages 101-112. ACM, 2011. Google Scholar
  19. D. Sabel and M. Schmidt-Schauß. Conservative concurrency in Haskell. In LICS'12, pages 561-570. IEEE, 2012. Google Scholar
  20. D. Sabel and M. Schmidt-Schauß. Contextual equivalence for the pi-calculus that can stop. Frank report 53, J. W. Goethe-Universität Frankfurt am Main, 2014. URL: http://www.ki.cs.uni-frankfurt.de/papers/frank/pi-stop-frank.pdf.
  21. D. Sangiorgi and D. Walker. The π-calculus: a theory of mobile processes. CUP, 2001. Google Scholar
  22. M. Schmidt-Schauß, C. Rau, and D. Sabel. Algorithms for Extended Alpha-Equivalence and Complexity. In RTA'13, volume 21 of LIPIcs, pages 255-270. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2013. Google Scholar
  23. M. Schmidt-Schauß and D. Sabel. Correctness of an STM Haskell implementation. In ICFP'13, pages 161-172. ACM, 2013. Google Scholar
  24. R. Thiemann and C. Sternagel. Certification of termination proofs using CeTA. In TPHOLs'09, volume 5674 of LNCS, pages 452-468. Springer, 2009. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact