An Introduction to Refinement Types


Ranjit Jhala (UCSD)

Whats this?


The First Bug


Page from Harvard Mark II log

A dead moth removed from the device

Fast forward to Present Day

Fast forward to Present Day

Fast forward to Present Day

Programming Languages Research

George Orwell (1984)

Modern Languages


F#

Rust

Scala

OCaml

Haskell

Modern Languages


Static Typing

First-class Functions

Immutability by Default

Modern Languages


Static Typing

First-class Functions

Immutability by Default


Make good designs easy and bad designs hard

Modern Languages?




Alas ... well-typed programs go very wrong!

Well-typed programs can go very wrong!


Well-typed programs can go very wrong!

Divide-by-zero

Keys missing in Maps

Pattern-match failures

Well-typed programs can go very wrong!

Divide-by-zero

Keys missing in Maps

Pattern-match failures

Buffer overflows (!)

Non-termination

Functional Correctness / Assertions...

Goal: Algorithmic Software Verification


Expressive

Verify program specific properties via domain specific analysis

Goal: Algorithmic Software Verification


Expressive

Verify program specific properties via domain specific analysis


Automatic

Rapid feedback to influence design, not only post-facto validation

Outline


Motivation