WG211/M13Hammond

Talk title: Using Dependent Types for Parallel Programming

Abstract: In this talk I will introduce a new approach to capture parallelism information directly in the type of a program. Using dependent types allows the parallel structure of a program to be captured in the program type .In this way, we can reason about the correctness of transformations for changing parallelism structures, as introduced by semi-automated refactoring process, for example. Moreover, it is also possible to capture timing information in the type, to relate this to the parallelism structure and to reason about improvements in timing behaviours, for example.