Journal article 1072 views 63 downloads
Defining Trace Semantics for CSP-Agda
Leibniz International Proceedings in Informatics, LIPIcs, Volume: 97, Pages: 12:1 - 12:23
Swansea University Author:
Anton Setzer
-
PDF | Accepted Manuscript
Released under the terms of a Creative Commons License (CC-BY).
Download (742.47KB)
DOI (Published version): 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 ha...
| Published in: | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| ISBN: | 978-3-95977-065-1 |
| ISSN: | 1868-8969 |
| Published: |
Dagstuhl, Germany
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
2018
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa38365 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| 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 The- ory, IO-Monad, Induction-Recursion, Interactive Program, Monad, Monadic Programming, Pro- cess Algebras, Sized Types, Universes, Trace Semantics |
| Start Page: |
12:1 |
| End Page: |
12:23 |