Joshua Dunfield(McGill University)
"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.
|Zeit:||Mittwoch, 03.03.2010, 14.00 Uhr|
|Ort:||Saarbrücken, Wartburg, Raum 410|
|Hinweis:||Der Vortrag wird live nach Kaiserslautern Gebäude 49, Raum 206 übertragen.|