A Lean library for algorithms and complexity

Algolean aims to formalise algorithms and complexity theory with a top-down approach. We build and use a lightweight Free-Monad based DSL which we call Prog. It allows and requires users to specifiy upfront, the basic operations that are counted and their cost models. The library is still at an early stage. It has all the pros and cons of using monads. Explore the source and generated documentation for definitions of queries, models, algorithms, and theorems.

Primary Focus

Algorithms & complexity theory

Core Idea

Explicit operations and costs. Free Monads