Write Some Idris
summary
Hands‑on workshop that teaches Idris by writing code not just theory: live use of Idris REPL, explicit proofs of equality (reflexive, transitive, congruence, injectivity), induction to prove n+0 = n, tactics and proof search, totality checks, and proof tactics that emit term witnesses. Demonstrates using Auto, Sigma/existentials, and the JS/C/LLVM/Java backends to produce executables. The capstone constructs a BF interpreter from a string‑literal proof (types index characters); compilation is shown but a final runtime test is left unresolved on the presenter’s Chromebook.
AI-written summary · about
chapters (18)
- 0:00Idris workshop intro
- 1:02Speaker and Idris basics
- 3:29Why Idris stands out
- 4:54Defining equality with types
- 8:10Proving simple equalities
- 15:24Working with holes
- 16:48Transitive property of equality
- 18:59Symmetry of equality proofs
- 23:16Congruence with equalities
- 25:03Induction for natural numbers
- 35:48Built-in equality and tactics
- 43:58Tactic-based proofs
- 51:08Idempotent and involution functions
- 1:03:23Proving impossibility with void
- 1:09:03Non-idempotent function proofs
- 1:23:43Identity function proof
- 1:28:01Dependently typed BF language
- 1:43:27Q&A
related talks
56mIdris: Programming with Dependent Types
01h 00mIntroduction to Coq - Part 1 of 2
26mInteractive Theorem Provers for Proof Education
35mProof Theory Impressionism: Blurring the Curry-Howard Line
01h 44mAn Introduction to Natural Deduction
49mCoding Tomorrow
01h 03mKeynote: Why Functional Programming Matters
44mKeynote Speaker - Simon Willison