Supporting inference in type-based verification
Speaker: Dimitrios Vytiniotis , Microsoft Research Cambridge
Date: March 11 2010
Time: 4:00PM to 5:00PM
Location: 32-G449
Host: Arvind and Robert Morris, MIT
Contact: Francis Doughty, 253-4602, doughty@mit.edu
Relevant URL: How do we reduce the cost of static verification for programmers?
Type systems offer a low-tech but effective means to achieve this:
Programmers express properties of programs using types; type checking
verifies that a program adheres to the specification that its type
expresses. Many traditional type systems cannot easily express data
invariants or pre/post-conditions, but compilers can conveniently
reconstruct all missing type information. On the other hand, type
reconstruction in more expressive and sophisticated type systems (such
as type systems with Generalized Algebraic Datatypes -- GADTs) is
often undecidable or non-modular. Programming in a fully explicit
fashion, where programmers provide all type information, is
prohibitive, so there is need for eliminating the uninformative
annotations.
This talk is about my work on bridging the gap between full type
reconstruction and fully explicitly typed programming in such
sophisticated type systems, now implemented in the Glasgow Haskell
Compiler: How do we implement and specify modular, predictable, and
economical (in terms of annotations) type inference in order to bring
the advantages of both worlds to programmers? I will present my initial
approach to type inference for GADTs and how it has benefited from the
introduction of implication constraints in more recent work. I will
show recent surprising results that indicate that ML-style
polymorphism may not scale to advanced type system features, and how
to work around these problems. I will finally describe ongoing work
on taking one step further: Engineering a type inference specification
and implementation to be parametric over a constraint domain without
giving up modularity and robustness. Alongside the main theme, this
talk will touch on some of my work on semantics and formal metatheory,
and will mention exciting ongoing work on game-based serialization and
ideas for future research.
Bio:
Dimitrios Vytiniotis is a Postdoctoral Researcher at Microsoft
Research Cambridge, working in the Programming Principles and Tools
group on programming languages. He has a PhD from the University of
Pennsylvania (2008), where he was supervised by Stephanie Weirich, and
an Electrical and Computer Engineering degree from the National
Technical University of Athens (2002). His interests span in the areas
of programming languages and functional programming, verification,
type systems, logic, and theory.
See other events that are part of CS Special Seminar Series Spring 2010
See other events happening in March 2010
