Making Types More Descriptive via Grading

by Dr. Dominic Orchard

Abstract

Many programming languages include a “type system” as a form of lightweight program verification which can eliminate bugs and aid programmer understanding. Traditionally such type systems characterise and categorise the data involved in a program, but many new type systems are being developed which capture program behaviour. Such “behavioural type systems” can futher guide the programmer, aiding them in avoiding bugs, and even more excitingly providing a specification from which a program can be algorithmically generated, at least in part. In this talk, I will explain and demonstrate a particular class of such behavioural types systems based on the recent idea of “graded types”. I’ll demo this technique in a practical setting, showing how we can constrain program behaviour via complex specifications, and sometimes even have parts of a program generated for us.

This talk will be pitched at undergraduate/postgraduate level and will include various programming examples in more than one language (spoiler: I will start with some assembly code!)

Bio

Dominic is a Lecturer at the School of Computing, University of Kent. He works mostly at the intersection between logic, semantics, and types, but also likes to be build programming systems. Dominic has an undergraduate degree in Computer Science from the University of Warwick and a PhD in Computer Science from the University of Cambridge. He worked as a Research Associate at Imperial College London and Cambridge before joining the University of Kent.

School of Computer and Cyber Sciences Augusta University