Refinement Types and Program Synthesis, Featuring Nadia Polikarpova
Every week @jeanqasaur hosts a really incredible Twitch stream where her and @hongyihu discuss programming language theory, and try to make it accessible to a wider audience. It always ends up being a great conversation, and fascinating links get shared in the chat. I want to try to capture and categorize some of those links, so that they're not lost when the stream ends.
This week, they interviewed Nadia Polikarpova about her very cool work with refinement types and program synthesis. A recording is temporarily available here.
Refinement Types and Liquid Types
An Introduction to Refinement Types - A quick video introduction to refinement types, by Ranjit Jhala
A Gentle Introduction to Liquid Types - An introduction to the motivations and use of liquid types
Liquid Types - The original 2008 paper discussing Liquid Types
Refinement Types for Typescript - A description of Refined Typescript, a lightweight refinement type system for TypeScript
Program Synthesis
CSE 291: Program Synthesis - A comprehensive introduction to program synthesis
Type-Driven Program Synthesis - A Strangeloop talk by Nadia, demonstrating the use of types in program synthesis
Synquid - Program Synthesis with Refinement Types - An online environment for interacting with Synquid, the program synthesis language introduced in the previous video
Lifty - A DSL for annotating sensitive data with security policies, verifying them at compile time, and automatically synthesizing corrections to detected bugs
General Programming
Chapel Parallel Programming Language - A programming language designed for productive parallel computing at scale.
Lasp Lang - A suite of Erlang libraries meant to support geo-distributed high-performance computing
Project Everest - A high-performance, standards-compliant, formally verified implementation of components in HTTPS ecosystem, including TLS
I'm hoping to make it a regular thing, but this is my first time sending out a newsletter, so let me know if it was or wasn't helpful, or if you have suggestions on how to present this information differently next time!
I hope you all have a great weekend!
- Quinn