Abstract

Abstract: A refinement type is a type qualified by a logical constraint; an example is the type of even numbers, that is, the type of integers qualified by the is-an-even-number constraint. Although this idea has been known in the research community for some time, it has been assumed impractical, because of the difficulties of constraint solving. But recent advances in automated reasoning have overturned this conventional wisdom, and transformed the idea into a practical design principle. I will present a primer on the design, implementation, and application of refinement types. I will explain:

• How a range of diverse features may be unified as instances of the general idea of refinement types.
• How a static checker for the Oslo modeling language M allows us to check for security errors in server configurations; intended constraints on configurations are expressed with refinement types, so that configuration validation reduces to type checking.
• How we statically check integrity and secrecy properties of security critical code, such as an implementation of the CardSpace security protocol, using a system of refinement types for the F# programming language.

Biography: Andy Gordon is a Principal Researcher at MSR Cambridge. His research interests are in the general area of programming languages. His work at Microsoft has involved applying type theory and other formal techniques to problems of computer security. His projects include the following: an analysis (with D. Syme) of the type system underlying the bytecode verifier of the Microsoft .NET Common Language Runtime; Cryptyc (with A. Jeffrey), a type-checker for cryptographic protocols; and the Samoa Project (with K. Bhargavan and C. Fournet) on formal tools for the security of XML Web Services. He is currently excited about the many possibilities of refinement types, and is actively developing them in the context of both F# and the Oslo Modeling Language M.