Source code for the TopHat implementation

DOI

Source code accompanying the paper:Steenvoorden, T.J., Naus, N. & Klinik, M. (2019). TopHat: A formal foundation for task-oriented programming. In E. Komendantskaya (Ed.), PPDP '19: Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019, Porto, Portugal — October 07 - 09, 2019 (pp. 1-13). New York: ACMDESCRIPTIONTopHat is a formalisation of Task Oriented Programming.This is the Haskell implementation of the language.CONTENTS- The language is specified as a GADT in Data.Task- Semantics, including all observations, can be found in Data.Task.Run- Main includes a couple of examples which can be executed.- More information on how to compile and run this program can be found in README.txtSHORT SUMMARYSoftware that models how people work is omnipresent in today's society. Current languages and frameworks often focus on usability by non-programmers, sacrificing flexibility and high level abstraction. Task-oriented programming (TOP) is a programming paradigm that aims to provide the desired level of abstraction while still being expressive enough to describe real world collaboration. It prescribes a declarative programming style to specify multi-user workflows. Workflows can be higher-order. They communicate through typed values on a local and global level. Such specifications can be turned into interactive applications for different platforms, supporting collaboration during execution. TOP has been around for more than a decade, in the forms of iTasks and mTasks, which are tailored for real-world usability. So far, it has not been given a formalisation which is suitable for formal reasoning.In this paper we give a description of the TOP paradigm and then decompose its rich features into elementary language elements, which makes them suitable for formal treatment. We use the simply typed lambda-calculus, extended with pairs and references, as a base language. On top of this language, we develop TopHat, a language for modular interactive workflows. We describe TopHat by means of a layered semantics. These layers consist of multiple big-step evaluations on expressions, and two labelled transition systems, handling user inputs.With TopHat we prepare a way to formally reason about TOP languages and programs. This approach allows for comparison with other work in the field. We have implemented the semantic rules of TopHat in Haskell, and the task layer on top of the iTasks framework. This shows that our approach is feasible, and lets us demonstrate the concepts by means of illustrative case studies. TOP has been applied in projects with the Dutch coast guard, tax office, and navy. Our work matters because formal program verification is important for mission-critical software, especially for systems with concurrency.

Identifier
DOI https://doi.org/10.17026/dans-zks-p82q
Metadata Access https://phys-techsciences.datastations.nl/oai?verb=GetRecord&metadataPrefix=oai_datacite&identifier=doi:10.17026/dans-zks-p82q
Provenance
Creator T.J. Steenvoorden; N. Naus; M.A.A. Klinik
Publisher DANS Data Station Phys-Tech Sciences
Contributor RU Radboud University
Publication Year 2020
Rights CC BY 4.0; info:eu-repo/semantics/openAccess; http://creativecommons.org/licenses/by/4.0
OpenAccess true
Contact RU Radboud University
Representation
Resource Type Dataset
Format application/octet-stream; text/xml; text/plain; application/zip; text/plain; charset=US-ASCII
Size 1357; 5710; 470; 26341; 8; 5021; 1528; 5300; 1925; 3356; 738; 1143; 8199; 46; 2170; 4329; 393; 161
Version 2.0
Discipline Other