Live-Coding Mathematics Your First Clojure Proof
summary
Live-coding shows a working Clojure proof assistant called LaTTe proof assistant that encodes Curry–Howard via lambda terms, lets you write proofs as Clojure code and type-check them in Emacs/Cider or Gorilla, and provides proof automation entry points so code can generate proof steps. Examples include a generic identity proof, a second-order encoding of conjunction with introduction/elimination derived for free, and a formal proof that injectivity survives composition where type-checking initially fails then succeeds.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:57Lambda calculus basics
- 5:43Typed lambda calculus
- 8:49Types and proofs
- 11:38Modus ponens and quantification
- 15:55Curry-Howard basics
- 19:19Natural deduction
- 30:26Latte library usage
- 38:27Function composition injectivity
- 40:37Conclusion
related talks
01h 34mFormal Logic Undressed
45mLogic Meta Programming for Functional Languages
33mHolbert: Reading, Writing, Proving and Learning in the Browser
38mLearn you some Lisp for Great Good
01h 02mSolving Problems the Clojure Way
40mFun with Functional Programming in Clojure
42mPractical Lambda Calculus
49mFun with the Lambda Calculus