Skip to main content
SpringerLink
Log in

A Coinductive Calculus for Asynchronous Side-Effecting Processes

  • Conference paper
Fundamentals of Computation Theory (FCT 2011)

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

Included in the following conference series:

Abstract

We present an abstract framework for concurrent processes in which atomic steps have generic side effects, handled according to the principle of monadic encapsulation of effects. Processes in this framework are potentially infinite resumptions, modelled using final coalgebras over the monadic base. As a calculus for such processes, we introduce a concurrent extension of Moggi’s monadic metalanguage of effects. We establish soundness and completeness of a natural equational axiomatisation of this calculus. Moreover, we identify a corecursion scheme that is explicitly definable over the base language and provides flexible expressive means for the definition of new operators on processes, such as parallel composition. As a worked example, we prove the safety of a generic mutual exclusion scheme using a verification logic built on top of the equational calculus.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bartels, F.: Generalised coinduction. Math. Structures in Comp. Sci. 13(2), 321–348 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  2. Benton, N., Hyland, M.: Traced premonoidal categories. ITA 37(4), 273–299 (2003)

    MathSciNet  MATH  Google Scholar 

  3. Bergstra, J.A., Klop, J.W.: The algebra of recursively defined processes and the algebra of regular processes. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol. 172, pp. 82–94. Springer, Heidelberg (1984)

    Chapter  Google Scholar 

  4. Capretta, V.: General recursion via coinductive types. Logical Methods in Computer Science 1(2) (2005)

    Google Scholar 

  5. Cenciarelli, P., Moggi, E.: A syntactic approach to modularity in denotational semantics. Technical report, Category Theory and Computer Science (1993)

    Google Scholar 

  6. Cockett, J.R.B.: Introduction to distributive categories. Mathematical Structures in Computer Science 3(3), 277–307 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  7. Crole, R.L., Pitts, A.M.: New foundations for fixpoint computations. In: Logic in Computer Science, LICS 1990, pp. 489–497. IEEE Computer Society Press, Los Alamitos (1990)

    Google Scholar 

  8. de Roever, W.P., de Boer, F.S., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge (2001)

    MATH  Google Scholar 

  9. Erkök, L., Launchbury, J.: Recursive monadic bindings. In: ICFP 2000, pp. 174–185. ACM, New York (2000)

    Google Scholar 

  10. Filinski, A.: On the relations between monadic semantics. Theor. Comp. Sci. 375, 41–75 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  11. Fiore, M.P., Moggi, E., Sangiorgi, D.: A fully abstract model for the π-calculus. Inf. Comput. 179(1), 76–117 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  12. Goncharov, S.: Kleene monads. PhD thesis, Universität Bremen (2010)

    Google Scholar 

  13. Harrison, W.L.: The essence of multitasking. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 158–172. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Harrison, W.L., Hook, J.: Achieving information flow security through monadic control of effects. J. Computer Security 17, 599–653 (2009)

    Article  Google Scholar 

  15. Hennessy, M., Plotkin, G.D.: Full abstraction for a simple parallel programming language. In: Becvar, J. (ed.) MFCS 1979. LNCS, vol. 74, pp. 108–120. Springer, Heidelberg (1979)

    Chapter  Google Scholar 

  16. Jacobs, B.: From coalgebraic to monoidal traces. Electron. Notes Theor. Comput. Sci. 264(2), 125–140 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  17. Jacobs, B., Poll, E.: Coalgebras and Monads in the Semantics of Java. Theoret. Comput. Sci. 291, 329–349 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  18. Krstić, S., Launchbury, J., Pavlovi, D.P.: Categories of processes enriched in final coalgebras. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 303–317. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  19. Milius, S., Palm, T., Schwencke, D.: Complete iterativity for algebras with effects. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 34–48. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  20. Milner, R.: Communication and concurrency. Prentice-Hall, Inc, Englewood Cliffs (1989)

    MATH  Google Scholar 

  21. Moggi, E.: Notions of computation and monads. Inf. Comput. 93, 55–92 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  22. Nicola, R.D., Hennessy, M.: Testing equivalence for processes. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 548–560. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  23. Papaspyrou, N., Macos, D.: A study of evaluation order semantics in expressions with side effects. J. Funct. Program. 10(3), 227–244 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  24. Peyton Jones, S. (ed.): Haskell 98 Language and Libraries — The Revised Report. Cambridge (2003); also: J. Funct. Programming  13, 2003.

    Google Scholar 

  25. Plotkin, G., Power, J.: Semantics for algebraic operations. In: Mathematical Foundations of Programming Semantics, MFPS 2001. ENTCS, vol. 45 (2001)

    Google Scholar 

  26. Rosenthal, K.I.: Quantales and their applications. Pitman Research Notes in Mathematics Series, vol. 234. Longman Scientific & Technical (1990)

    Google Scholar 

  27. Rutten, J.: Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249, 3–80 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  28. Schröder, L., Mossakowski, T.: Monad-independent dynamic logic in HasCASL. J. Logic Comput. 14, 571–619 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  29. Schröder, L., Mossakowski, T.: HasCASL: Integrated higher-order specification and program development. Theor. Comput. Sci. 410(12-13), 1217–1260 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  30. Syme, D., Granicz, A., Cisternino, A.: Expert F#. Apress (2007)

    Google Scholar 

  31. Tolmach, A.P., Antoy, S.: A monadic semantics for core Curry. In: WFLP 2003. ENTCS, vol. 86(3), pp. 16–34 (2003)

    Google Scholar 

  32. Uustalu, T.: Generalizing substitution. ITA 37(4), 315–336 (2003)

    MathSciNet  MATH  Google Scholar 

  33. Wadler, P.: How to declare an imperative. ACM Computing Surveys 29, 240–263 (1997)

    Article  Google Scholar 

  34. Worrell, J.: Terminal sequences for accessible endofunctors. In: Coalgebraic Methods in Computer Science, CMCS 1999. ENTCS, vol. 19 (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Safe and Secure Cognitive Systems, DFKI GmbH, Bremen, Germany

    Sergey Goncharov & Lutz Schröder

Authors
  1. Sergey Goncharov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lutz Schröder
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics, University of Oslo, Postboks 1080 Blindern, 0316, Oslo, Norway

    Olaf Owe  & Martin Steffen  & 

  2. Department of Informatics, University of Bergen, Postboks 7800, 5020, Bergen, Norway

    Jan Arne Telle

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goncharov, S., Schröder, L. (2011). A Coinductive Calculus for Asynchronous Side-Effecting Processes. In: Owe, O., Steffen, M., Telle, J.A. (eds) Fundamentals of Computation Theory. FCT 2011. Lecture Notes in Computer Science, vol 6914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22953-4_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22953-4_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22952-7

  • Online ISBN: 978-3-642-22953-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation