The Mastermind behind Refinement Types
summary
Example: a sublist function needs index constraints like 0 <= i < j <= length and the compiler should prove those at compile time. SMT solvers follow a CDCL(T) architecture pairing a SAT engine with theory solvers, answering sat/unsat/unknown; mixing integer multiplication makes many queries undecidable in practice. Practical toolchains discussed include Liquid Haskell backed by Z3, and a Lean integration: an SMT tactic published in May and Lean’s built‑in green tactic from September, both working but sometimes returning unknown.
AI-written summary · about
chapters (8)
- 0:00SMT solvers and refinement types
- 5:00Propositional to first-order logic
- 14:12SMT solvers and theories
- 19:34How SMT solvers work
- 25:43Core SMT theories
- 30:23Dependent types vs SMT
- 32:29Interactive and automated proving
- 34:43Conclusion and future
related talks
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
30mAnalyzing Programs with SMT Solvers
35mA Peek Inside SAT Solvers
18mConcrete Type Inference for Code Optimization using Machine Learning with SMT S...
46mRefinement Types from Light to Deep Verification
33mSolving constraints during type inference
27mCompiling higher-order specifications to SMT solvers: how to deal with rejection ...
29mExplicit Refinement Types