Daniel's Blog

Advent of Code in Coq

Series status: Suspended

First post in 2020, last post in 2021

In this series, I apply the Coq proof assistant to formalize solutions to the puzzles to Advent of Code 2020. That is, I try to solve the problem, and formally prove that the solution is correct.