Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Fri 28 Aug 2020 15:00 - 15:30 at Haskell - Paper Session 5 - Types Chair(s): Jurriaan Hage

Using dependent types in production code is a practical way to eliminate errors. While there are many examples of using dependent Haskell to prove invariants about code, few of these are applied to large scale production systems. Critics claim that dependent types are only useful in toy examples and that they are impractical for use in the real world. This experience report analyzes real world examples where dependent types have enabled us to find and eliminate bugs in production Haskell code.

I work for Facebook in the Programming Languages and Runtimes group. My current projects involve adding capabilities to the Hack programming language that will allow us to guarantee the privacy of user data. In the past, I have also worked on large scale production systems implemented in Haskell.

Before working at Facebook, I was an undergrad at the University of Pennsylvania. During my time at Penn, I worked on a project to verify the type safety System FC using the Coq Proof Assistant. This project was advised by Stephanie Weirich and Richard Eisenberg.

Fri 28 Aug

Displayed time zone: Eastern Time (US & Canada) change

14:30 - 16:00
Paper Session 5 - TypesHaskell at Haskell
Chair(s): Jurriaan Hage Utrecht University, Netherlands
14:30
30m
Talk
Staged Sums of Products
Haskell
Matthew Pickering University of Bristol, UK, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, UK
DOI
15:00
30m
Talk
Eliminating Bugs with Dependent Haskell (Experience Report)
Haskell
Noam Zilberstein Facebook, USA
DOI
15:30
30m
Talk
Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)
Haskell
DOI File Attached