Logic & formal methods
Logic and formal verification: proof assistants, Coq, Lean, TLA+, type theory and proofs, SAT solvers, model checking, program correctness, foundations of mathematics, set theory.
Recommended videos
- Brian Beckman: Don't fear the Monad
- 28c3: The Science of Insecurity
- "Propositions as Types" by Philip Wadler
- Math's Fundamental Flaw
- The Banach–Tarski Paradox
- The Future of Mathematics?
- Leslie Lamport: Thinking Above the Code
- How To Count Past Infinity
- "Finding bugs without running or even looking at code" by Jay Parlar
- Edwin Brady - Idris 2 - Type-driven Development of Idris
- Infinity is bigger than you think - Numberphile
- 2017 ACM PPoPP Keynote: It's Time for a New Old Language
- Edwin Brady - Idris 2: Type-driven development of Idris | Code Mesh LDN 18
- "A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram
- Hillel Wayne - Beyond Unit Tests: Taking Your Testing to the Next Level - PyCon 2018
- Lec 1 | MIT 6.042J Mathematics for Computer Science, Fall 2010
- What if Current Foundations of Mathematics are Inconsistent? | Vladimir Voevodsky
- "Tackling Concurrency Bugs with TLA+" by Hillel Wayne
- MIT Godel Escher Bach Lecture 1
- A Tour of Prolog
- Philip Wadler - Propositions as Types (Lambda Days 2016)
- Barliman: trying the halting problem backwards, blindfolded - William Byrd, Greg Rosenblatt
- "Type-Driven Program Synthesis" by Nadia Polikarpova
- "A Little Taste of Dependent Types" by David Christiansen