IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2010 > Verifying Functional Programs with Type Refinements
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Joshua Dunfield

miércoles 24 de febrero de 2010

11:00am IMDEA conference room

Joshua Dunfield, Researcher, McGill University, Montreal

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.