Dominic Orchard - Quantitative program reasoning in Granule via graded modal types | Code Mesh LDN

---

QUANTITATIVE PROGRAM REASONING IN GRANULE VIA GRADED MODAL TYPES
by Dominic Orchard

THIS TALK IN THREE WORDS:
Types
for
Verification

TALK LEVEL: Intermediate

ABSTRACT
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. We'll see examples enforcing privacy constraints, stateful protocols, and verifying properties of standard functional programs just by getting the right type signature.

---

THE SPEAKER - DOMINIC ORCHARD
Computer science lecturer and co-creator of the Granule language

Dominic is a computer science researcher and lecturer, interested in mathematically structured programming and lots else, at the School of Computing, University of Kent

---

CODE SYNC & CODE MESH LDN 19
Code Mesh LDN is powered by Code Sync. Code Mesh LDN 19 was sponsored by WhatsApp, Microsoft, Erlang Solutions, Juxt, aeternity, Duffel, and IOHK.

CODE SYNC

#Granule #FunctionalProgramming