Nathan Taylor on Liquid Type Systems [PWL NYC]

We're pleased to present Nathan Taylor on Liquid Types. (Read the paper: https://goto.ucsd.edu/~rjhala/liquid/...) --- We'd like to thank Datadog for making the PWL NYC meetup possible! Join the Pack https://careers.datadoghq.com/ --- Type systems are great! When you write a well-typed program, you've an assurance that certain facts about your program will always be true; at no point is a string passed to a function that expects an tuple argument, nor will one that is supposed to return an array have a corner case where it actually returns an int. The more expressive your type system is, the more specific those certain facts can be - a type system that supports generics can specify what type the keys and values of an dictionary must be, but for example, still couldn't specify that each element is an even integer. We'd need a more expressive type system for that! Programming language researchers are interested in exploring different ways to add expressivity to type systems without sacrificing usability. Liquid Types, published at PLDI in 2008, combines traditional type theory techniques with SMT solvers from the automated theorem prover research community to form a fascinating point in the design space. We'll begin by discussing the broader context around the work, learn a bit about how to digest an academic type theory paper, and then work through the details of the paper with the help of a toy implementation of the technique. Nathan Taylor is a PhD student at UT Austin, where he ponders the intersection of formal methods and distributed systems. Before joining UT, he spent a decade in industry hacking on systems software ranging from GPU simulators, to JIT compilers and garbage collectors, up to distributed databases and edge computing networks. He was additionally a developer at Microsoft Research, a lecturer at MacEwan University and the University of Toronto, and a repeat speaker at Papers We Love SF.