Nathan Taylor on Liquid Type Systems

We're pleased to present Nathan Taylor on Liquid Types. (Read the paper)

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.

---

⚠️ Required: You must have your real name on your account and provide a photo ID at the entrance to attend, per the venue rules. If you are not on the list, you will not be admitted.

🚔 Reminder: Papers We Love has a code of conduct. Breaching the CoC is grounds to be ejected from the meetup at the organizers' discretion.

📹 The event will be recorded and made available 1-2 weeks afterwards.

💬 Join us on the Papers We Love Discord - https://discord.gg/6gupsBg4qp

Venue:

Datadog
620 8th Ave, 45th Floor
New York, NY 10018 USA
Doors open at 6:30pm EST
Note: Enter the building on 8th Avenue and go to the reception desk on your left

⚠️ Required: You must have your real name on your Meetup account and provide a photo ID at the entrance to attend, per the venue rules. If you are not on the list, you will not be admitted.