Formal Logic Undressed
summary
Workshop loads Coq and PeaCoq and encodes Knights-and-Knaves puzzles as propositions, then builds step‑by‑step proofs with tactics like destruct, intros and apply before collapsing them with automation (the firstorder tactic). It asserts the Curry‑Howard link—types as propositions, programs as proofs—and shows how untyped lambda calculus yields inconsistency (Y combinator) so typing enforces soundness. It also outlines an unboxed sum via De Morgan and demonstrates the proofs succeed.
AI-written summary · about
chapters (8)
- 0:00Start
- 4:52An Informal Formal Logic Workshop
- 6:36I Have a Proposition for You
- 8:28George Boole
- 10:39Augustus De Morgan
- 12:10Charles Lutwidge Dodgson
- 15:14Bertrand Russell Alfred North Whitehead
- 18:07Raymond Smullyan Alonzo Church's student
related talks
52mWhat logic can teach us, Scala programmers
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
31mA Coq Library of Undecidable Problems
19mType Inference Logics
41mLiving inside a Theorem Proving Universe
42mLive-Coding Mathematics Your First Clojure Proof
11mPOPLMark reloaded: Mechanizing proofs by logical relations
18mEpistemic Logic for Polyglots (Short Paper)