Semantic Equivalence of Task-Oriented Programs in TopHat

Tosca Klijnsma, Tim Steenvoorden*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review


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 languageEnglish
Title of host publicationTrends in Functional Programming - 23rd International Symposium, TFP 2022, Revised Selected Papers
EditorsWouter Swierstra, Nicolas Wu
PublisherSpringer Nature
Number of pages26
ISBN (Electronic)9783031213144
ISBN (Print)9783031213137
Publication statusPublished - 2022
Event23rd International Symposium on Trends in Functional Programming, TFP 2022 - Virtual, Online
Duration: 17 Mar 202218 Mar 2022

Publication series

SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13401 LNCS


Symposium23rd International Symposium on Trends in Functional Programming, TFP 2022
Internet address


  • Formal semantics
  • Program equivalence
  • Task-oriented programming


Dive into the research topics of 'Semantic Equivalence of Task-Oriented Programs in TopHat'. Together they form a unique fingerprint.

Cite this