Document Open Access Logo

Defining Trace Semantics for CSP-Agda

Authors Bashar Igried, Anton Setzer

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2016.12.pdf
  • Filesize: 0.66 MB
  • 23 pages

Document Identifiers

Author Details

Bashar Igried
Anton Setzer

Cite AsGet BibTex

Bashar Igried and Anton Setzer. Defining Trace Semantics for CSP-Agda. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2016.12

Abstract

This article is based on the library CSP-Agda, which represents the process algebra CSP coinductively in the interactive theorem prover Agda. The intended application area of CSP-Agda is the proof of properties of safety critical systems (especially the railway domain). In CSP-Agda, CSP processes have been extended to monadic form, allowing the design of processes in a more modular way. In this article we extend the trace semantics of CSP to the monadic setting. We implement this semantics, together with the corresponding refinement and equality relation, formally in CSP-Agda. In order to demonstrate the proof capabilities of CSP-Agda, we prove in CSP-Agda selected algebraic laws of CSP based on the trace semantics. Because of the monadic settings, some adjustments need to be made to these laws. The examples covered in this article are the laws of refinement, commutativity of interleaving and parallel, and the monad laws for the monadic extension of CSP. All proofs and definitions have been type checked in Agda. Further proofs of algebraic laws will be available in the repository of CSP-Agda.
Keywords
  • Agda
  • CSP
  • Coalgebras
  • Coinductive Data Types
  • Dependent Type Theory
  • IO-Monad
  • Induction-Recursion
  • Interactive Program
  • Monad
  • Monadic Programming,

Metrics

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

References

  1. Andreas Abel. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universität München, 2006. URL: http://www2.tcs.ifi.lmu.de/~abel/publications.html.
  2. Andreas Abel. Compositional coinduction with sized types. In Ichiro Hasuo, editor, Coalgebraic Methods in Computer Science, pages 5-10. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-40370-0_2.
  3. Andreas Abel, Stephan Adelsberger, and Anton Setzer. ooAgda, 2016. URL: https://github.com/agda/ooAgda.
  4. Andreas Abel, Stephan Adelsberger, and Anton Setzer. Interactive programming in Agda - Objects and graphical user interfaces. Journal of Functional Programming, 27, Jan 2017. URL: http://dx.doi.org/10.1017/S0956796816000319.
  5. Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: Programming infinite structures by observations. In Roberto Giacobazzi and Radhia Cousot, editors, Proceedings of POPL'13, pages 27-38. ACM, 2013. URL: http://dx.doi.org/10.1145/2429069.2429075.
  6. Agda Community. The Agda Wiki, 2017. URL: http://wiki.portal.chalmers.se/agda/pmwiki.php.
  7. Agda Community. Literal Agda, 2017. URL: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda.
  8. JCM Baeten, Dirk Albert van Beek, and JE Rooda. Process algebra. Handbook of Dynamic System Modeling, pages 19-1, 2007. URL: http://mate.tue.nl/mate/pdfs/8509.pdf.
  9. J. A. Bergstra and J. W. Klop. Fixed point semantics in process algebras. CWI technical report, Stichting Mathematisch Centrum. Informatica-IW 206/82, 1982. URL: http://oai.cwi.nl/oai/asset/6750/6750A.pdf.
  10. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda - a functional language with dependent types. In Proceedings of TPHOLs '09, pages 73-78. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-03359-9_6.
  11. Thierry Coquand. Infinite objects in type theory. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, volume 806 of LNCS, pages 62-78. Springer, 1994. URL: http://dx.doi.org/10.1007/3-540-58085-9_72.
  12. Peter Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In Gérard Huet and Gordon Plotkin, editors, Logical frameworks, pages 280-306. Cambridge University Press, 1991. URL: http://www.cse.chalmers.se/~peterd/papers/Setsem_Inductive.pdf.
  13. Peter Dybjer. Universes and a general notion of simultaneous inductive-recursive definition in type theory. In Bengt Nordström, Kent Petersson, and Gordon Plotkin, editors, Proceedings of the 1992 workshop on types for proofs and programs, Båstad, June 1992. URL: http://www.lfcs.inf.ed.ac.uk/research/types-bra/proc/proc92.ps.gz.
  14. Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525-549, June 2000. URL: http://dx.doi.org/10.2307/2586554.
  15. Peter Dybjer and Anton Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124:1-47, 2003. URL: http://dx.doi.org/10.1016/S0168-0072(02)00096-9.
  16. ERTMS. The European Rail Traffic Mangement System, 2013. URL: http://www.ertms.net/.
  17. P. Hancock and A. Setzer. The IO monad in dependent type theory. In Electronic proceedings of the workshop on dependent types in programming, Göteborg, 27-28 March 1999, 1999. URL: http://www.md.chalmers.se/Cs/Research/Semantics/APPSEM/dtp99.html.
  18. Peter Hancock and Anton Setzer. Interactive programs in dependent type theory. In P. Clote and H. Schwichtenberg, editors, Computer Science Logic, LNCS, Vol. 1862, pages 317-331, 2000. URL: http://dx.doi.org/10.1007/3-540-44622-2_21.
  19. Peter Hancock and Anton Setzer. Specifying interactions with dependent types. In Workshop on subtyping and dependent types in programming, Portugal,7 July 2000, 2000. URL: http://www-sop.inria.fr/oasis/DTP00/Proceedings/proceedings.html.
  20. C. A. R. Hoare. Communicating sequential processes. Commun. ACM, 21(8):666-677, 1978. URL: http://dx.doi.org/10.1145/359576.359585.
  21. Bashar Igried and Anton Setzer. CSP-Agda. Agda library, 2016. URL: http://www.cs.swan.ac.uk/~csetzer/software/agda2/cspagda/.
  22. Bashar Igried and Anton Setzer. Programming with monadic CSP-style processes in dependent type theory. In Proceedings of the 1st International Workshop on Type-Driven Development, TyDe 2016, pages 28-38, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2976022.2976032.
  23. Bashar Igried and Anton Setzer. Trace and stable failures semantics for csp-agda. In Ekaterina Komendantskaya and John Power, editors, Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types, Edinburgh, UK, 28-29 November 2016, volume 258 of Electronic Proceedings in Theoretical Computer Science, pages 36-51. Open Publishing Association, 2017. URL: http://dx.doi.org/10.4204/EPTCS.258.3.
  24. Karim Kanso. Agda as a Platform for the Development of Verified Railway Interlocking Systems. PhD thesis, Dept. of Computer Science, Swansea University, Swansea, UK, August 2012. URL: http://cs.swan.ac.uk/~cskarim/files/.
  25. Karim Kanso and Anton Setzer. A light-weight integration of automated and interactive theorem proving. Mathematical Structures in Computer Science, FirstView:1-25, 12 November 2014. URL: http://dx.doi.org/10.1017/S0960129514000140.
  26. Per Martin-Löf. Intuitionistic type theory. Bibliopolis, Naples, 1984. ISBN: 88-7088-105-9. Google Scholar
  27. Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55-92, 1991. URL: http://dx.doi.org/10.1016/0890-5401(91)90052-4.
  28. A. W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1997. ISBN: 0136744095. Google Scholar
  29. Steve Schneider. Concurrent and Real Time Systems: The CSP Approach. John Wiley, 1st edition, 1999. ISBN: 978-0-471-62373-1. Google Scholar
  30. Anton Setzer. Object-oriented programming in dependent type theory. In Conference Proceedings of TFP 2006, 2006. URL: http://www.cs.swan.ac.uk/~csetzer/index.html.
  31. Anton Setzer, Andreas Abel, Brigitte Pientka, and David Thibodeau. Unnesting of copatterns. In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi, volume 8560 of LNCS, pages 31-45. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08918-8_3.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact