Quantitative program reasoning in Granule via graded modal types

A benefit of static typing is that various program properties can be specified and automatically checked as part of a language. But there are always limits to what can be expressed.

This talk presents Granule, a functional language which pushes these limits by combining linear and indexed types with the recent notion of graded modal types. Dominic will share examples enforcing privacy constraints, stateful protocols, and verifying properties of standard functional programs just by getting the right type signature.

THIS TALK IN THREE WORDS

Types

for

Verification

OBJECTIVES

• Understand how linearity can be used to rule out various program errors.
• Understand how graded modal types provide a way, on top of linearity, to do even more program verification.

TARGET AUDIENCE

People curious about the latest results in type systems.