Quantitative program reasoning in Granule via graded modal types
summary
Granule implements a functional language combining linear, indexed and graded modal types with a working REPL and typechecker that uses an automated theorem prover backend (Z3/CVC4). Types express exact usage counts (naturals and intervals like 0..1), let a value’s type determine how many times a function is called (replicate 5), and tie vector lengths to behavior. A security lattice (e.g. private/public lattice) enforces data-leak prevention. Implementation works for the demos but complex constraints can hit solver timeouts; source is on GitHub.
AI-written summary · about
chapters (9)
- 0:00Start
- 3:46Protocol of Interaction
- 4:29Linear Logic
- 15:55Graded Modality
- 23:27Index Types
- 26:53Dependent Types
- 38:42Privacy Example
- 41:12Syntax Errors
- 44:00Graded Monad
related talks
32mGranite: Compositional Functional Logic Programming
27mPractical Extensions for Graded Monads
20mA Graded Modal Type Theory for Pulse Schedules
49mSemantic Foundations for Probabilistic Programming
20mTowards Graded Modal Dependent Types
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
34mGraded Monads and Type-Level Programming for Dependence Analysis
19mCombining Dependency, Grades, and Adjoint Logic