No Cover Image

Conference Paper/Proceeding/Abstract 422 views 54 downloads

Programming with monadic CSP-style processes in dependent type theory / Anton, Setzer

TyDe 2016, Pages: 28 - 38

Swansea University Author: Anton, Setzer

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 2019-05-13T12:56:18Z
id cronfa29413
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-05-11T20:27:33.4401174</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><lastEdited>2019-05-11T20:27:33.4401174</lastEdited><Created>2016-08-02T18:29:19.0891910</Created><path><level id="1">College of Science</level><level id="2">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><action/><embargoDate>2016-12-02T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect></document></documents></rfc1807>
spelling 2019-05-11T20:27:33.4401174 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 2019-05-11T20:27:33.4401174 2016-08-02T18:29:19.0891910 College of 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
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 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://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:44:55Z
_version_ 1650781476307861504
score 10.868663