Lean
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
- 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
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.