PubSub implementation in Haskell with formal verification in Coq
This addresses software correctness in cloud messaging systems, but appears incremental as it applies existing formal verification methods to a specific pattern.
The paper tackled implementing the PubSub messaging pattern for cloud-based Software as a Service in Haskell and formally verifying its correctness using Coq, presenting an example implementation and proof.
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.