DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2016.12

Defining Trace Semantics for CSP-Agda

Authors: Bashar Igried and Anton Setzer

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{igried_et_al:LIPIcs.TYPES.2016.12,
  author =	{Igried, Bashar and Setzer, Anton},
  title =	{{Defining Trace Semantics for CSP-Agda}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.12},
  URN =		{urn:nbn:de:0030-drops-98509},
  doi =		{10.4230/LIPIcs.TYPES.2016.12},
  annote =	{Keywords: Agda, CSP, Coalgebras, Coinductive Data Types, Dependent Type Theory, IO-Monad, Induction-Recursion, Interactive Program, Monad, Monadic Programming,}
}

Search Results

Documents authored by Igried, Bashar

Defining Trace Semantics for CSP-Agda

Abstract

Cite as

Thanks for your feedback!

Could not send message