Daniel's Blog

Implementing and Verifying "Static Program Analysis" in Agda

Series status: Ongoing

First post in 2024, last post in 2024

In this series, I attempt to formalize the first few chapters of Static Program Analysis in Agda. The goal is to have a formally verified, yet executable, static analyzer for a simple language.