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!
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.
Keywords: Agda, CSP, Dependent Type Theory, Monadic Programming, Process Algebras, Interactive Program, Monad, IO-Monad, Coalgebras, Coinductive Data Types, Sized Types, Induction-Recursion, Universes.
College: Faculty of Science and Engineering
Start Page: 28
End Page: 38

Similar Items