Dimitrios Vytiniotis, Microsoft Research Cambridge

Type system support for static program verification

Abstract: Advanced type system features, such as Generalized Algebraic Datatypes (GADTs), Type Functions, and impredicative polymorphism have proven to be invaluable programming language extensions for enforcing data invariants and for verifying program correctness. Unfortunately, integrating those features in mainstream languages that support modular type inference poses tough theoretical, implementation, and design problems.

In this talk I will present my previous and ongoing work towards addressing those problems. I will emphasize on type inference with implication constraints induced by pattern matching and equalities induced by programmer-declared function axioms. Since full type inference for those features is undecidable and the ``natural'' specifications lack principal types this work is towards a decidable high-level type system specification that is (i) not overly-demanding in terms of user type annotations, and (ii) only accepts programs that can be assigned principal types. I will finally describe ongoing work on taking that approach one step further: engineering a type checker and constraint solver to be parametric over a domain-specific programmer-supplied constraint solver, without losing modular and predictable type inference.

Bio:

Dimitrios Vytiniotis is currently a Postdoctoral Researcher at Microsoft Research Cambridge, working with the Programming Principles and Tools group on programming languages. He holds a PhD from the University of Pennsylvania (2008) and an Electrical and Computer Engineering degree from the National Technical University of Athens (2002). His interests span in the areas of programming languages, type systems, functional programming, formal methods, software verification, logic, and theory.