Modal μ-Calculus for Free

The process of using formal verification, in order to ensure that a piece of software meets it functional requirements consists of three main steps: designing a model of the given piece of software, translating the functional requirements, which the piece of software must satisfy, into properties of said model and verifying that the model...

Monadic approach to Serverless Applications

The serverless computing trend is steadily picking up steam over the last few years and is challenging the traditional microservices on Kubernetes model which included inefficiencies like idling. The big three cloud providers AWS, GCP and Azure have different opinions on what serverless computing and serverless applications should look like, how...

The monad and examples from Haskell: A computer-checked library for Category Theory in Lean

Category Theory is a widely used field of Mathematics.<br/>Some concepts from it are often used in functional programming.<br/>This paper will focus on the Monad and a few implementations of it from Haskell.<br/>We will also present the computer-checked library we have written to help us in this task.

Deriving Effect Handler Semantics

For algebraic effects and handlers, we know both small-step and big-step operational semantics and we are familiar with denotational semantics. But, what is missing is a structured showing that one is equivalent to the other. On top of this, most efficient implementations of algebraic effects and handlers closely resemble their denotational...

Towards Modular Compilation Using Higher-Order Effects

Compilers transform a human readable source language into machine readable target language. Nanopass compilers simplify this approach by breaking up this transformation into small steps that are more understandable, maintainable, and extensible. We propose a semantics-driven variant of the nanopass compiler architecture exploring the use a...

Cloud Monads: A novel concept for monadic abstraction over state in serverless cloud applications

Serverless computing is a relatively recent paradigm that promises fine-grained billing and ease-of-use by abstracting away cloud infrastructure for developers. There is an increasing interest in using the serverless paradigm to execute data analysis tasks. Serverless functions often interact with external services, which can be considered...

From definitional interpreter to symbolic executor

Symbolic execution is a technique for automatic software validation and verification. New symbolic executors regularly appear for both existing and new languages and such symbolic executors are generally manually (re)implemented each time we want to support a new language. We propose to automatically generate symbolic executors from language...