Semantic Equivalence of Task-Oriented Programs in TopHat

Tosca Klijnsma; Tim Steenvoorden

doi:10.1007/978-3-031-21314-4_6

Semantic Equivalence of Task-Oriented Programs in TopHat

Tosca Klijnsma
, Tim Steenvoorden^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Abstract

Task-oriented programming (top) is a new programming paradigm for specifying multi-user workflows. To reason formally about top programs, a formal language called TopHat has been designed, together with its operational semantics. For proving properties about task-oriented programs, it is desirable to know when two TopHat-programs are semantically equivalent. This paper aims to answer this question. We show that a task can be in either one of five conditions, and for every two tasks in the same condition, we define what it means for them to be semantically equivalent. Using this definition, we study a number of transformation laws for TopHat-programs, which can be used by developers and compilers to optimise top-programs. We show that the operation on types in TopHat is a functor but cannot be a monad. We support our findings with proofs formalised in the dependently typed programming language Idris.

Original language	English
Title of host publication	Trends in Functional Programming - 23rd International Symposium, TFP 2022, Revised Selected Papers
Editors	Wouter Swierstra, Nicolas Wu
Publisher	Springer Nature
Pages	100-125
Number of pages	26
ISBN (Electronic)	9783031213144
ISBN (Print)	9783031213137
DOIs	https://doi.org/10.1007/978-3-031-21314-4_6
Publication status	Published - 2022
Event	23rd International Symposium on Trends in Functional Programming, TFP 2022 - Virtual, Online Duration: 17 Mar 2022 → 18 Mar 2022 https://trendsfp.github.io/2022/

Publication series

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13401 LNCS
ISSN	0302-9743

Symposium

Symposium	23rd International Symposium on Trends in Functional Programming, TFP 2022
Period	17/03/22 → 18/03/22
Internet address	https://trendsfp.github.io/2022/

Keywords

Formal semantics
Program equivalence
Task-oriented programming

Access to Document

10.1007/978-3-031-21314-4_6Licence: CC BY

Cite this

Klijnsma, Tosca ; Steenvoorden, Tim. / Semantic Equivalence of Task-Oriented Programs in TopHat. Trends in Functional Programming - 23rd International Symposium, TFP 2022, Revised Selected Papers. editor / Wouter Swierstra ; Nicolas Wu. Springer Nature, 2022. pp. 100-125 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13401 LNCS).

@inproceedings{22f12e9e3c0744f5b313e9e6922bc427,

title = "Semantic Equivalence of Task-Oriented Programs in TopHat",

abstract = "Task-oriented programming (top) is a new programming paradigm for specifying multi-user workflows. To reason formally about top programs, a formal language called TopHat has been designed, together with its operational semantics. For proving properties about task-oriented programs, it is desirable to know when two TopHat-programs are semantically equivalent. This paper aims to answer this question. We show that a task can be in either one of five conditions, and for every two tasks in the same condition, we define what it means for them to be semantically equivalent. Using this definition, we study a number of transformation laws for TopHat-programs, which can be used by developers and compilers to optimise top-programs. We show that the operation on types in TopHat is a functor but cannot be a monad. We support our findings with proofs formalised in the dependently typed programming language Idris.",

keywords = "Formal semantics, Program equivalence, Task-oriented programming",

author = "Tosca Klijnsma and Tim Steenvoorden",

note = "Publisher Copyright: {\textcopyright} 2022, The author(s).; 23rd International Symposium on Trends in Functional Programming, TFP 2022 ; Conference date: 17-03-2022 Through 18-03-2022",

year = "2022",

doi = "10.1007/978-3-031-21314-4\_6",

language = "English",

isbn = "9783031213137",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Nature",

pages = "100--125",

editor = "Wouter Swierstra and Nicolas Wu",

booktitle = "Trends in Functional Programming - 23rd International Symposium, TFP 2022, Revised Selected Papers",

address = "United States",

url = "https://trendsfp.github.io/2022/",

}

Klijnsma, T & Steenvoorden, T 2022, Semantic Equivalence of Task-Oriented Programs in TopHat. in W Swierstra & N Wu (eds), Trends in Functional Programming - 23rd International Symposium, TFP 2022, Revised Selected Papers. Springer Nature, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13401 LNCS, pp. 100-125, 23rd International Symposium on Trends in Functional Programming, TFP 2022, 17/03/22. https://doi.org/10.1007/978-3-031-21314-4_6

Semantic Equivalence of Task-Oriented Programs in TopHat. / Klijnsma, Tosca; Steenvoorden, Tim.
Trends in Functional Programming - 23rd International Symposium, TFP 2022, Revised Selected Papers. ed. / Wouter Swierstra; Nicolas Wu. Springer Nature, 2022. p. 100-125 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13401 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Semantic Equivalence of Task-Oriented Programs in TopHat

AU - Klijnsma, Tosca

AU - Steenvoorden, Tim

PY - 2022

Y1 - 2022

N2 - Task-oriented programming (top) is a new programming paradigm for specifying multi-user workflows. To reason formally about top programs, a formal language called TopHat has been designed, together with its operational semantics. For proving properties about task-oriented programs, it is desirable to know when two TopHat-programs are semantically equivalent. This paper aims to answer this question. We show that a task can be in either one of five conditions, and for every two tasks in the same condition, we define what it means for them to be semantically equivalent. Using this definition, we study a number of transformation laws for TopHat-programs, which can be used by developers and compilers to optimise top-programs. We show that the operation on types in TopHat is a functor but cannot be a monad. We support our findings with proofs formalised in the dependently typed programming language Idris.

AB - Task-oriented programming (top) is a new programming paradigm for specifying multi-user workflows. To reason formally about top programs, a formal language called TopHat has been designed, together with its operational semantics. For proving properties about task-oriented programs, it is desirable to know when two TopHat-programs are semantically equivalent. This paper aims to answer this question. We show that a task can be in either one of five conditions, and for every two tasks in the same condition, we define what it means for them to be semantically equivalent. Using this definition, we study a number of transformation laws for TopHat-programs, which can be used by developers and compilers to optimise top-programs. We show that the operation on types in TopHat is a functor but cannot be a monad. We support our findings with proofs formalised in the dependently typed programming language Idris.

KW - Formal semantics

KW - Program equivalence

KW - Task-oriented programming

UR - https://dblp.org/rec/conf/sfp/KlijnsmaS22

U2 - 10.1007/978-3-031-21314-4_6

DO - 10.1007/978-3-031-21314-4_6

M3 - Conference Article in proceeding

AN - SCOPUS:85148008987

SN - 9783031213137

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 100

EP - 125

BT - Trends in Functional Programming - 23rd International Symposium, TFP 2022, Revised Selected Papers

A2 - Swierstra, Wouter

A2 - Wu, Nicolas

PB - Springer Nature

T2 - 23rd International Symposium on Trends in Functional Programming, TFP 2022

Y2 - 17 March 2022 through 18 March 2022

ER -

Klijnsma T, Steenvoorden T. Semantic Equivalence of Task-Oriented Programs in TopHat. In Swierstra W, Wu N, editors, Trends in Functional Programming - 23rd International Symposium, TFP 2022, Revised Selected Papers. Springer Nature. 2022. p. 100-125. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13401 LNCS). doi: 10.1007/978-3-031-21314-4_6

Semantic Equivalence of Task-Oriented Programs in TopHat

Abstract

Publication series

Symposium

Keywords

Access to Document

Other files and links

Fingerprint

Cite this