Skip to main content
SpringerLink
Log in
Book cover

International Conference on Relational and Algebraic Methods in Computer Science

RAMICS 2017: Relational and Algebraic Methods in Computer Science pp 274–289Cite as

Tower Induction and Up-to Techniques for CCS with Fixed Points

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10226))

Abstract

We present a refinement of Pous’ companion-based coinductive proof technique and apply it to CCS with general fixed points. We construct companions based on inductive towers and thereby obtain a powerful induction principle. Our induction principle implies a new sufficient condition for soundness of up-to techniques subsuming respectfulness and compatibility. For bisimilarity in CCS, companions yield a notion of relative bisimilarity. We show that relative bisimilarity is a congruence, a basic result implying soundness of bisimulation up to context. The entire development is constructively formalized in Coq.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Adams, R.: Formalized metatheory with terms represented by an indexed family of types. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 1–16. Springer, Heidelberg (2006). doi:10.1007/11617990_1

    Chapter  Google Scholar 

  2. Altenkirch, T., Chapman, J., Uustalu, T.: Monads need not be endofunctors. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 297–311. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12032-9_21

    Chapter  Google Scholar 

  3. Bauer, A., Lumsdaine, P.L.: On the Bourbaki-Witt principle in toposes. In: Mathematical Proceedings of the Cambridge Philosophical Society, vol. 155, pp. 87–99. Cambridge University Press (2013)

    Google Scholar 

  4. Davey, B., Priestley, H.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002)

    Book  MATH  Google Scholar 

  5. Hur, C.-K., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: The 40th Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 23–25 January 2013, pp. 193–206 (2013)

    Google Scholar 

  6. Xavier, L.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  7. Milner, R.: Communication and Concurrency, vol. 84. Prentice Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  8. Parrow, J., Weber, T.: The largest respectful function. Log. Methods Comput. Sci. 12(2) (2016)

    Google Scholar 

  9. Pataraia, D.: A constructive proof of Tarski’s fixed-point theorem for dcpo’s. Presented in the 65th Peripatetic Seminar on Sheaves and Logic, Aarhus, Denmark, November 1997

    Google Scholar 

  10. Pous, D.: Weak bisimulation up to elaboration. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 390–405. Springer, Heidelberg (2006). doi:10.1007/11817949_26

    Chapter  Google Scholar 

  11. Pous, D.: Complete lattices and up-to techniques. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 351–366. Springer, Heidelberg (2007). doi:10.1007/978-3-540-76637-7_24

    Chapter  Google Scholar 

  12. Pous, D.: Coinduction all the way up. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 307–316. ACM, New York (2016)

    Google Scholar 

  13. Sangiorgi, D.: On the bisimulation proof method. Math. Struct. Comput. Sci. 8(5), 447–479 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  14. Schäfer, S., Smolka, G., Tebbi, T.: Completeness and decidability of de Bruijn substitution algebra in Coq. In: Proceedings of the Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, 15–17 January 2015, pp. 67–73. ACM (2015)

    Google Scholar 

  15. Smolka, G., Schäfer, S., Doczkal, C.: Transfinite constructions in classical type theory. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 391–404. Springer, Cham (2015). doi:10.1007/978-3-319-22102-1_26

    Google Scholar 

  16. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285–309 (1955)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Saarland University, Saarbrücken, Germany

    Steven Schäfer & Gert Smolka

Authors
  1. Steven Schäfer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gert Smolka
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Steven Schäfer .

Editor information

Editors and Affiliations

  1. Data61, CSIRO, Sydney, New South Wales, Australia

    Peter Höfner

  2. CNRS, Lyon, France

    Damien Pous

  3. University of Sheffield, Sheffield, United Kingdom

    Georg Struth

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Schäfer, S., Smolka, G. (2017). Tower Induction and Up-to Techniques for CCS with Fixed Points. In: Höfner, P., Pous, D., Struth, G. (eds) Relational and Algebraic Methods in Computer Science. RAMICS 2017. Lecture Notes in Computer Science(), vol 10226. Springer, Cham. https://doi.org/10.1007/978-3-319-57418-9_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-57418-9_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-57417-2

  • Online ISBN: 978-3-319-57418-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation