Theorem prover lab: applications in programming languages

Lambda the Ultimate SSA: Optimizing Functional Programs in SSA

Numerical packages in lean

Webserver example. Custom syntax

novice friendly induction tactic

metaprogramming framework for formal verification lean4

“The Lean typeclass resolution procedure can be viewed as a simple λ-Prolog interpreter [8], where the Horn clauses are the user declared instances.” That sounds fun


elan tool


lake is a new build tool on the horizon

Using nix is kind of a pain. I haven’t done it.