No Cover Image

Conference Paper/Proceeding/Abstract 1388 views 294 downloads

Programming with monadic CSP-style processes in dependent type theory

Bashar Igried, Anton Setzer Orcid Logo

TyDe 2016, Pages: 28 - 38

Swansea University Author: Anton Setzer Orcid Logo

DOI (Published version): 10.1145/2976022.2976032

Abstract

We introduce a library called CSP-Agda for representing processes in the dependently typed theorem prover and interactive programming language Agda. We will enhance processes by a monad structure. The monad structure facilitates combining processes in a modular way, and allows to define recursion as...

Full description

Published in: TyDe 2016
ISBN: 978-1-4503-4435-7
Published: ACM 2016
Online Access: http://www.cs.swan.ac.uk/~csetzer/articles/TyDe2016.pdf
URI: https://cronfa.swan.ac.uk/Record/cronfa29413
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2016-08-02T19:01:24Z
last_indexed 2020-06-25T18:39:34Z
id cronfa29413
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2020-06-25T15:43:18.2632042</datestamp><bib-version>v2</bib-version><id>29413</id><entry>2016-08-02</entry><title>Programming with monadic CSP-style processes in dependent type theory</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>2016-08-02</date><deptcode>SCS</deptcode><abstract>We introduce a library called CSP-Agda for representing processes in the dependently typed theorem prover and interactive programming language Agda. We will enhance processes by a monad structure. The monad structure facilitates combining processes in a modular way, and allows to define recursion as a direct operation on processes. Processes are defined coinductively as non-well-founded trees. The nodes of the tree are formed by a an atomic one step relation, which determines for a process the external, internal choices, and termination events it can choose, and whether the process has terminated. The data type of processes is inspired by Setzer and Hancock's notion of interactive programs in dependent type theory. The operators of CSP will be defined rather than atomic operations, and compute new elements of the data type of processes from existing ones. The approach will make use of advanced type theoretic features: the use of inductive-recursively defined universes; the definition of coinductive types by their observations, which has similarities to the notion of an object in object-oriented programming; the use of sized types for coinductive types, which allow coinductive definitions in a modular way; the handling of finitary information (names of processes) in a coinductive settings; the use of named types for automatic inference of arguments similar to its use in template Meta-programming in C++; and the use of interactive programs in dependent type theory.We introduce a simulator as an interactive program in Agda. The simulator allows to observe the evolving of processes following external or internal choices. Our aim is to use this in order to simulate railway interlocking system and write programs in Agda which directly use CSP processes.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>TyDe 2016</journal><paginationStart>28</paginationStart><paginationEnd>38</paginationEnd><publisher>ACM</publisher><isbnElectronic>978-1-4503-4435-7</isbnElectronic><keywords>Agda, CSP, Dependent Type Theory, Monadic Programming, Process Algebras, Interactive Program, Monad, IO-Monad, Coalgebras, Coinductive Data Types, Sized Types, Induction-Recursion, Universes.</keywords><publishedDay>19</publishedDay><publishedMonth>9</publishedMonth><publishedYear>2016</publishedYear><publishedDate>2016-09-19</publishedDate><doi>10.1145/2976022.2976032</doi><url>http://www.cs.swan.ac.uk/~csetzer/articles/TyDe2016.pdf</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2020-06-25T15:43:18.2632042</lastEdited><Created>2016-08-02T18:29:19.0891910</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><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>0029413-02122016130722.pdf</filename><originalFilename>p28-igried.pdf</originalFilename><uploaded>2016-12-02T13:07:22.4170000</uploaded><type>Output</type><contentLength>447332</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><embargoDate>2016-12-02T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2020-06-25T15:43:18.2632042 v2 29413 2016-08-02 Programming with monadic CSP-style processes in dependent type theory 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2016-08-02 SCS We introduce a library called CSP-Agda for representing processes in the dependently typed theorem prover and interactive programming language Agda. We will enhance processes by a monad structure. The monad structure facilitates combining processes in a modular way, and allows to define recursion as a direct operation on processes. Processes are defined coinductively as non-well-founded trees. The nodes of the tree are formed by a an atomic one step relation, which determines for a process the external, internal choices, and termination events it can choose, and whether the process has terminated. The data type of processes is inspired by Setzer and Hancock's notion of interactive programs in dependent type theory. The operators of CSP will be defined rather than atomic operations, and compute new elements of the data type of processes from existing ones. The approach will make use of advanced type theoretic features: the use of inductive-recursively defined universes; the definition of coinductive types by their observations, which has similarities to the notion of an object in object-oriented programming; the use of sized types for coinductive types, which allow coinductive definitions in a modular way; the handling of finitary information (names of processes) in a coinductive settings; the use of named types for automatic inference of arguments similar to its use in template Meta-programming in C++; and the use of interactive programs in dependent type theory.We introduce a simulator as an interactive program in Agda. The simulator allows to observe the evolving of processes following external or internal choices. Our aim is to use this in order to simulate railway interlocking system and write programs in Agda which directly use CSP processes. Conference Paper/Proceeding/Abstract TyDe 2016 28 38 ACM 978-1-4503-4435-7 Agda, CSP, Dependent Type Theory, Monadic Programming, Process Algebras, Interactive Program, Monad, IO-Monad, Coalgebras, Coinductive Data Types, Sized Types, Induction-Recursion, Universes. 19 9 2016 2016-09-19 10.1145/2976022.2976032 http://www.cs.swan.ac.uk/~csetzer/articles/TyDe2016.pdf COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2020-06-25T15:43:18.2632042 2016-08-02T18:29:19.0891910 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Bashar Igried 1 Anton Setzer 0000-0001-5322-6060 2 0029413-02122016130722.pdf p28-igried.pdf 2016-12-02T13:07:22.4170000 Output 447332 application/pdf Version of Record true 2016-12-02T00:00:00.0000000 true
title Programming with monadic CSP-style processes in dependent type theory
spellingShingle Programming with monadic CSP-style processes in dependent type theory
Anton Setzer
title_short Programming with monadic CSP-style processes in dependent type theory
title_full Programming with monadic CSP-style processes in dependent type theory
title_fullStr Programming with monadic CSP-style processes in dependent type theory
title_full_unstemmed Programming with monadic CSP-style processes in dependent type theory
title_sort Programming with monadic CSP-style processes in dependent type theory
author_id_str_mv 5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Anton Setzer
author2 Bashar Igried
Anton Setzer
format Conference Paper/Proceeding/Abstract
container_title TyDe 2016
container_start_page 28
publishDate 2016
institution Swansea University
isbn 978-1-4503-4435-7
doi_str_mv 10.1145/2976022.2976032
publisher ACM
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://www.cs.swan.ac.uk/~csetzer/articles/TyDe2016.pdf
document_store_str 1
active_str 0
description We introduce a library called CSP-Agda for representing processes in the dependently typed theorem prover and interactive programming language Agda. We will enhance processes by a monad structure. The monad structure facilitates combining processes in a modular way, and allows to define recursion as a direct operation on processes. Processes are defined coinductively as non-well-founded trees. The nodes of the tree are formed by a an atomic one step relation, which determines for a process the external, internal choices, and termination events it can choose, and whether the process has terminated. The data type of processes is inspired by Setzer and Hancock's notion of interactive programs in dependent type theory. The operators of CSP will be defined rather than atomic operations, and compute new elements of the data type of processes from existing ones. The approach will make use of advanced type theoretic features: the use of inductive-recursively defined universes; the definition of coinductive types by their observations, which has similarities to the notion of an object in object-oriented programming; the use of sized types for coinductive types, which allow coinductive definitions in a modular way; the handling of finitary information (names of processes) in a coinductive settings; the use of named types for automatic inference of arguments similar to its use in template Meta-programming in C++; and the use of interactive programs in dependent type theory.We introduce a simulator as an interactive program in Agda. The simulator allows to observe the evolving of processes following external or internal choices. Our aim is to use this in order to simulate railway interlocking system and write programs in Agda which directly use CSP processes.
published_date 2016-09-19T03:35:46Z
_version_ 1763751542155902976
score 11.037056

Similar Items