Graded Monads and Type-Level Programming for Dependence Analysis
Programmers make assumptions about the order of memory operations, which are not captured in the operations’ types and therefore cannot be enforced statically by a compiler. This can lead programmers to accidentally violate those assumptions if they are not careful. To address this issue, we encode the memory locations that are accessed by a given computation using a graded monad. We use the data flow dependencies which arise from this to construct a type-level graph that we analyse to automatically order the computations so that no dependencies are violated. This also allows for computations which have no dependencies on each other to be run concurrently.
Thu 26 AugDisplayed time zone: Seoul change
23:30 - 01:00
|Design Patterns for Parser Combinators (Functional Pearl)|
|Graded Monads and Type-Level Programming for Dependence Analysis|
Jurriaan Hage Utrecht University, Netherlands