Joshua Dunfield

"Verifying Functional Programs with Type Refinements"

Types express properties of programs; typechecking is specification checking. But the specifications expressed by conventional type systems are imprecise. Type refinements enable programmers to express more precise properties, while keeping typechecking decidable.

I present a system that unifies and extends past work on datasort and index refinements. Intersection and union types permit a powerful type system that requires no user input besides type annotations. Instead of seeing type annotations as a burden or just as a shield against undecidability, I see them as a desirable form of machine-checked documentation. Accordingly, I embrace the technique of bidirectional typechecking for everything from dimension types to first-class polymorphism.

My implementation of this type system, for a subset of Standard ML, found several bugs in the SML/NJ data structure libraries.

Bio: Joshua Dunfield received his PhD from Carnegie Mellon University in 2007 for his work on type refinements, intersection and union types. He is presently a postdoctoral fellow at McGill University in Montreal. His research interests include type-based verification, typed compilation, dependent types, functional programming, proof assistants and programming environments.