No Cover Image

Journal article 230 views 2 downloads

Defining Trace Semantics for CSP-Agda / Bashar Igried; Anton Setzer

Leibniz International Proceedings in Informatics, LIPIcs, Volume: 97, Pages: 12:1 - 12:23

Swansea University Author: Setzer, Anton

  • basharIgriedAntonSetzerTypes2016Postproceedings.pdf

    PDF | Accepted Manuscript

    Released under the terms of a Creative Commons License (CC-BY).

    Download (742.47KB)

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

Full description

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
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
College: College of Science
Start Page: 12:1
End Page: 12:23