No Cover Image

Journal article 1208 views 84 downloads

Defining Trace Semantics for CSP-Agda

Bashar Igried, Anton Setzer Orcid Logo

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

Swansea University Author: Anton Setzer Orcid Logo

  • basharIgriedAntonSetzerTypes2016Postproceedings.pdf

    PDF | Accepted Manuscript

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

    Download (742.47KB)

Check full text

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

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 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!
first_indexed 2018-02-01T05:33:42Z
last_indexed 2018-12-10T20:14:33Z
id cronfa38365
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2018-12-10T14:57:50.3604611</datestamp><bib-version>v2</bib-version><id>38365</id><entry>2018-01-31</entry><title>Defining Trace Semantics for CSP-Agda</title><swanseaauthors><author><sid>5f7695285397f46d121207120247c2ae</sid><ORCID>0000-0001-5322-6060</ORCID><firstname>Anton</firstname><surname>Setzer</surname><name>Anton Setzer</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2018-01-31</date><deptcode>SCS</deptcode><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.</abstract><type>Journal Article</type><journal>Leibniz International Proceedings in Informatics, LIPIcs</journal><volume>97</volume><paginationStart>12:1</paginationStart><paginationEnd>12:23</paginationEnd><publisher>Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik</publisher><placeOfPublication>Dagstuhl, Germany</placeOfPublication><isbnElectronic>978-3-95977-065-1</isbnElectronic><issnElectronic>1868-8969</issnElectronic><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</keywords><publishedDay>30</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2018</publishedYear><publishedDate>2018-11-30</publishedDate><doi>10.4230/LIPIcs.TYPES.2016.12</doi><url>http://drops.dagstuhl.de/opus/volltexte/2018/9850/pdf/LIPIcs-TYPES-2016-12.pdf</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2018-12-10T14:57:50.3604611</lastEdited><Created>2018-01-31T22:42:59.7374053</Created><authors><author><firstname>Bashar</firstname><surname>Igried</surname><order>1</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>2</order></author></authors><documents><document><filename>0038365-26072018021200.pdf</filename><originalFilename>basharIgriedAntonSetzerTypes2016Postproceedings.pdf</originalFilename><uploaded>2018-07-26T02:12:00.1230000</uploaded><type>Output</type><contentLength>700300</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2018-12-10T00:00:00.0000000</embargoDate><documentNotes>Released under the terms of a Creative Commons License (CC-BY).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2018-12-10T14:57:50.3604611 v2 38365 2018-01-31 Defining Trace Semantics for CSP-Agda 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2018-01-31 SCS 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. Journal Article Leibniz International Proceedings in Informatics, LIPIcs 97 12:1 12:23 Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik Dagstuhl, Germany 978-3-95977-065-1 1868-8969 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 30 11 2018 2018-11-30 10.4230/LIPIcs.TYPES.2016.12 http://drops.dagstuhl.de/opus/volltexte/2018/9850/pdf/LIPIcs-TYPES-2016-12.pdf COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2018-12-10T14:57:50.3604611 2018-01-31T22:42:59.7374053 Bashar Igried 1 Anton Setzer 0000-0001-5322-6060 2 0038365-26072018021200.pdf basharIgriedAntonSetzerTypes2016Postproceedings.pdf 2018-07-26T02:12:00.1230000 Output 700300 application/pdf Accepted Manuscript true 2018-12-10T00:00:00.0000000 Released under the terms of a Creative Commons License (CC-BY). true eng
title Defining Trace Semantics for CSP-Agda
spellingShingle Defining Trace Semantics for CSP-Agda
Anton Setzer
title_short Defining Trace Semantics for CSP-Agda
title_full Defining Trace Semantics for CSP-Agda
title_fullStr Defining Trace Semantics for CSP-Agda
title_full_unstemmed Defining Trace Semantics for CSP-Agda
title_sort Defining Trace Semantics for CSP-Agda
author_id_str_mv 5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Anton Setzer
author2 Bashar Igried
Anton Setzer
format Journal article
container_title Leibniz International Proceedings in Informatics, LIPIcs
container_volume 97
container_start_page 12:1
publishDate 2018
institution Swansea University
isbn 978-3-95977-065-1
issn 1868-8969
doi_str_mv 10.4230/LIPIcs.TYPES.2016.12
publisher Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
url http://drops.dagstuhl.de/opus/volltexte/2018/9850/pdf/LIPIcs-TYPES-2016-12.pdf
document_store_str 1
active_str 0
description 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.
published_date 2018-11-30T03:48:32Z
_version_ 1763752345256067072
score 11.036706

Similar Items