Logic and Mechanized Reasoning

Theorem prover lab: applications in programming languages

Lambda the Ultimate SSA: Optimizing Functional Programs in SSA

Numerical packages in lean

Webserver example. Custom syntax https://github.com/leanprover/lean4/blob/master/tests/playground/webserver/Webserver.lean

novice friendly induction tactic https://arxiv.org/pdf/2012.08990.pdf

metaprogramming framework for formal verification https://dl.acm.org/doi/pdf/10.1145/3110278

http://leanprover.github.io/papers/lean4.pdf 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

Aesop (Automated Extensible Search for Obvious Proofs) i


elan tool


lake is a new build tool on the horizon

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