PubSub implementation in Haskell with formal verification in Coq

TL;DR

This paper presents a Haskell implementation of the PubSub messaging pattern for cloud-based SaaS applications, along with a formal correctness proof using Coq, demonstrating the integration of functional programming and theorem proving for reliable cloud services.

Contribution

It introduces a novel approach to implementing PubSub in Haskell with formal verification in Coq, ensuring correctness in cloud messaging systems.

Findings

Successful implementation of PubSub in Haskell

Formal proof of correctness in Coq

Potential for reliable cloud messaging solutions

Abstract

In the cloud, the technology is used on-demand without the need to install anything on the desktop. Software as a Service is one of the many cloud architectures. The PubSub messaging pattern is a cloud-based Software as a Service solution used in complex systems, especially in the notifications part where there is a need to send a message from one unit to another single unit or multiple units. Haskell is a generic typed programming language which has pioneered several advanced programming language features. Based on the lambda calculus system, it belongs to the family of functional programming languages. Coq, also based on a stricter version of lambda calculus, is a programming language that has a more advanced type system than Haskell and is mainly used for theorem proving i.e. proving software correctness. This paper aims to show how PubSub can be used in conjunction with cloud computing (Software as a Service), as well as to present an example implementation in Haskell and proof of correctness in Coq.