Daniel Marshall
PhD student and graded types enthusiast
Daniel is currently a PhD student at the University of Kent in the south of England; they are working on the Granule project, which aims to discover how to capture more properties about how programs compute (rather than just what they compute) at the type level. Prior to this they attained an MComp degree in Computer Science and Mathematics in their hometown a little further north, from the University of Sheffield.
Daniel is particularly interested in type theory and programming language implementation, and works on extending the (already very powerful) idea of graded types underlying the Granule language to be able to precisely describe ideas like memory management and communication safety, by finding connections with research on concepts such as ownership types and session types.
A Hitchhiker's Guide to Linearity
Ever since Girard came up with linear logic back in the 1980s, computer scientists have been trying to figure out how to bring the idea of linearity into the realm of programming languages in order to demonstrate benefits in the real world.
Nowadays, there are enough languages starting to take inspiration from linear logic to make your head spin; whether it's linear types in Haskell, uniqueness types in Clean, quantitative types in Idris, or the ownership system in Rust, there seems to be a different approach for everyone - but which is right for you?
In this talk, we'll take a whirlwind tour through the design space. I'll explain the strengths and weaknesses of each of these ideas and show you how mixing and matching them can help to improve both safety and performance when working with resources such as file handles, mutable arrays, and communication channels, taking lessons from my ongoing work towards unifying these various concepts in our very own research language, Granule.
AUDIENCE:
The target audience for this talk is mixed; I aim to present an inclusive talk that is both aimed at people who are familiar with, say, linear types in Haskell or the ownership system in Rust, which will help them to understand how this relates to the systems used by other languages and how they can access the strengths of those systems through their own preferred language of choice, but also is valuable to people who have never seen this kind of type system before, and will help them to understand the power offered by these ideas.
SlidesVideo ←Back
