Principles and applications of refinement types

Add to your list(s) Download to your calendar using vCal

• Andy Gordon (Microsoft Research)
• Wednesday 01 July 2009, 13:30-14:30
• Large public lecture room, Microsoft Research, Roger Needham Building, 7 J J Thomson Avenue, Cambridge CB3 0FB.

If you have a question about this talk, please contact Dr Fabien Petitcolas.

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.

This talk is part of the Microsoft Research Summer School series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge University Engineering Department Talks
• Featured lists
• Large public lecture room, Microsoft Research, Roger Needham Building, 7 J J Thomson Avenue, Cambridge CB3 0FB
• Methodology in design research
• Microsoft Research Cambridge, public talks
• Microsoft Research Summer School
• School of Technology
• de239's list

Note that ex-directory lists are not shown.