<

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

Dominic Orchard
Code Mesh LDN
07 Nov 2019
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.