Free Generalized Monoids for Programming and Proving

Programmer productivity is key in today's software development: broader functionality must be provided on more projects, in less time and with fewer developers. Yet, productivity often suffers because programmers structure and reason about their programs in an ad-hoc manner.

This project aims to remedy the situation by applying concepts from category theory, an abstract branch of mathematics, to systematically structure programs. More specifically, we study the class of concepts known as free generalized monoids. One member of this class, free monads, is gaining traction among functional programming researchers and industrial practitioners, but many others are waiting to be discovered and put to good use.

We will unlock the potential of free generalized monoids for programmers and programming language developers/researchers by 1) researching optimal ways of representing and interpreting free structures for different purposes, 2) demonstrating their utility for different advanced applications (quantitative information flow, smart contracts, ...), 3) developing tools for processing and 4) reasoning about programming languages.

The results of our work provide programmers and researchers with methodologies and tools for structuring their programs and proofs with free generalized monoids. This provides an accessible and systematic approach enabling greater flexibility and expressiveness without unnecessary incidental complexity.