Campus Event Calendar
Event Entry
What and Who
Verifying Functional Programs with Type Refinements
Joshua Dunfield
McGill University
SWS Colloquium
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.
SWS, RG1
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 3 March 2010
14:00
60 Minutes
MPI SWS
5th floor
Saarbrücken
Abstract
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.
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.
Contact
Bettina Bennett
0631-9303 9602
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
206
passcode not visible
logged in users only
Rose Hoberman, 05/07/2010 14:40
Bettina Peden-Bennett, 03/11/2010 14:33 -- Created document.
Bettina Peden-Bennett, 03/11/2010 14:33 -- Created document.