Dominic Orchard
Lecturer @ University of Kent
Dominic is a lecturer and researcher in the Programming Languages and Systems group at the University of Kent. His research centers on programming language approaches to reasoning, often leveraging types in a functional setting. His lecturing typically spans functional programming, logic, and theory.
Past Activities
Code Mesh LDN
16.25 - 17.10
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.