Type Inference For TLA+ in Apalache

on YouTube ↗40m

" summary

Apalache ships two standalone tools: a type checker that performs local analysis and asks for a few annotations (used in the CarTalkPuzzle demo with four annotations) and a prototype type inference engine that needs no annotations and runs globally. The inference runs on 35 community specs (extended to 42 with minimal fixes), completes under a second for most and about 10s for a 1,100-line outlier, automatically finds real bugs (Raft), rejects mixed function/sequence uses (Queens), and cannot soundly type some dynamic‑style patterns (DijkstraMutex).

AI-written summary · about

" chapters (18)

1. 0:00Intro
2. 0:50Symbolic model checker for TLA
3. 8:41Uninterpreted types
4. 10:03Type annotations for the built-in operators
5. 13:39Type checking becomes equation solving
6. 15:11Type unification
7. 16:22Boundaries of type checking
8. 17:14Talk Outline
9. 18:24Our Approach by Example
10. 22:52Experiments - Benchmark Sizes
11. 23:29Experiments - Type Inference Times
12. 24:41Interesting Benchmarks
13. 28:32FOL Encoding Examples
14. 29:36Type-Term Compatibility Examples
15. 31:04Types of Built-in Operators
16. 34:05Constraints From Schemas
17. 38:26Recovery Theorem
18. 39:16Conclusion