About

Think of this website as a collection of entries defining concepts in Agda or another similar language, like Lean for example. It is not a blog, really, but a library to me.

The entries are mostly about PLT constructs and concepts that I'm currently trying to understand for my actual job, or that I find interesting and popular and wish to adopt for future modelling and verification.

The idea of this website, look-and-feel and structure is inspired by the work in anoma/nspec and Juvix. I'm actually writing another plugin for MkDocs to support Agda inspired by the plugin for supporting literate Juvix to produce the pages you see. The plugin is currently in revision and not open. I plan to share it once I'm satisfied with it.