Lean

Logic and Mechanized Reasoning

Theorem prover lab: applications in programming languages

Lambda the Ultimate SSA: Optimizing Functional Programs in SSA

Numerical packages in lean

• numlean
• lean karray

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

• lean 4 Advent of Code 2021
• lean4 raytracer
• balance car
• lean 4 talk overview second half
• Theorem proving in lean4
• lean 4 manual

• lean 3 logic and proof

• functional programming in lean Christianson
• theorme prover lab

Aesop (Automated Extensible Search for Obvious Proofs) i

Build

elan tool

leanpkg

lake is a new build tool on the horizon

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