No Cover Image

Journal article 231 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!
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:50Z</datestamp><bib-version>v2</bib-version><id>38365</id><entry>2018-01-31</entry><title>Defining Trace Semantics for CSP-Agda</title><alternativeTitle></alternativeTitle><author>Anton Setzer</author><firstname>Anton</firstname><surname>Setzer</surname><active>true</active><ORCID>0000-0001-5322-6060</ORCID><ethesisStudent>false</ethesisStudent><sid>5f7695285397f46d121207120247c2ae</sid><email>61db1ab5eaeff34062db71cc1973df39</email><emailaddr>QBY4tVYqSovxQSx/NwDRpMjwe531u+mO/3IG3xe5jMg=</emailaddr><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><journalNumber/><paginationStart>12:1</paginationStart><paginationEnd>12:23</paginationEnd><publisher>Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik</publisher><placeOfPublication>Dagstuhl, Germany</placeOfPublication><isbnPrint/><isbnElectronic>978-3-95977-065-1</isbnElectronic><issnPrint/><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>0</publishedDay><publishedMonth>0</publishedMonth><publishedYear>0</publishedYear><publishedDate>0001-01-01</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></notes><college>College of Science</college><department>Computer Science</department><CollegeCode>CSCI</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution/><researchGroup>Theoretical Computer Science</researchGroup><supervisor/><sponsorsfunders/><grantnumber/><degreelevel/><degreename>None</degreename><lastEdited>2018-12-10T14:57:50Z</lastEdited><Created>2018-01-31T22:42:59Z</Created><path><level id="1">College of Science</level><level id="2">Computer Science</level></path><authors><author><firstname>Bashar</firstname><surname>Igried</surname><orcid/><order>1</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid/><order>2</order></author></authors><documents><document><filename>0038365-26072018021200.pdf</filename><originalFilename>basharIgriedAntonSetzerTypes2016Postproceedings.pdf</originalFilename><uploaded>2018-07-26T02:12:00Z</uploaded><type>Output</type><contentLength>700300</contentLength><contentType>application/pdf</contentType><version>AM</version><cronfaStatus>true</cronfaStatus><action>Published to Cronfa</action><actionDate>10/12/2018</actionDate><embargoDate>2018-12-10T00:00:00</embargoDate><documentNotes>Released under the terms of a Creative Commons License (CC-BY).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents></rfc1807>
spelling 2018-12-10T14:57:50Z v2 38365 2018-01-31 Defining Trace Semantics for CSP-Agda Anton Setzer Anton Setzer true 0000-0001-5322-6060 false 5f7695285397f46d121207120247c2ae 61db1ab5eaeff34062db71cc1973df39 QBY4tVYqSovxQSx/NwDRpMjwe531u+mO/3IG3xe5jMg= 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 0 0 0 0001-01-01 10.4230/LIPIcs.TYPES.2016.12 http://drops.dagstuhl.de/opus/volltexte/2018/9850/pdf/LIPIcs-TYPES-2016-12.pdf College of Science Computer Science CSCI SCS Theoretical Computer Science None 2018-12-10T14:57:50Z 2018-01-31T22:42:59Z College of Science Computer Science Bashar Igried 1 Anton Setzer 2 0038365-26072018021200.pdf basharIgriedAntonSetzerTypes2016Postproceedings.pdf 2018-07-26T02:12:00Z Output 700300 application/pdf AM true Published to Cronfa 10/12/2018 2018-12-10T00:00:00 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
Setzer, Anton
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_***_Setzer, Anton
author Setzer, Anton
author2 Bashar Igried
Anton Setzer
format Journal article
container_title Leibniz International Proceedings in Informatics, LIPIcs
container_volume 97
container_start_page 12:1
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
college_str College of Science
hierarchytype
hierarchy_top_id collegeofscience
hierarchy_top_title College of Science
hierarchy_parent_id collegeofscience
hierarchy_parent_title College of Science
department_str Computer Science{{{_:::_}}}College of Science{{{_:::_}}}Computer Science
url http://drops.dagstuhl.de/opus/volltexte/2018/9850/pdf/LIPIcs-TYPES-2016-12.pdf
document_store_str 1
active_str 1
researchgroup_str Theoretical Computer Science
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 0001-01-01T15:55:34Z
_version_ 1642760539501232128
score 11.061451