Lectures on Principles and Applications of Refinement Types

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.

The lectures in this series are based on recent research with my esteemed colleagues Karthik Bhargavan, Gavin Bierman, and Cédric Fournet of MSR Cambridge, and David Langworthy of the Microsoft Connected Systems Division; much of our work relies on the excellent Z3 automated theorem prover developed by Nikolaj Bjorner and Leonardo de Moura of MSR Redmond. 

Speaker

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.

Resources

  • F7 – an enhanced typechecker for the F# programming language [link]
  • Oslo and the modeling language M [link]
  • Z3 – the  MSR SMT solver [link]
  • Liquid types – type inference for refinement types [link]
  • Slides used at Marktoberdorf [link]
  • Tutorial notes for the Marktoberdorf proceedings [link]

 

Schedule

My lectures are in two formats: an overview (45 minutes or so), and a three hour course (which begins with the overview).

  • 090212 4pm (overview): Information Security Group, Royal Holloway University of London, Egham, UK [link]
  • 090219 2pm (course): Colloquium, School of Computing Science, University of Newcastle, Newcastle, UK [link]
  • 090226 12:30pm (overview): TechFest'09, Cascade Room, Building 33, Microsoft Campus, Redmond, WA, USA [internal link]
  • 090317 9am (course): Winter School on Hot Topics in Distributed Computing, La Plagne, France [link]
  • 090407 9am (overview): British Colloquium for Theoretical Computer Science, Warwick, UK [link]
  • 090522 1pm (overview): PL Club, CIS, University of Pennsylvania, USA
  • 090608 4pm (overview): Seminar, Department of Computer Science, University of Pisa, Italy
  • 090701 1:30pm (overview): Microsoft Research Summer School, MSR Cambridge, UK [link]
  • 090804-16 (course): 30th International Summer School Marktoberdorf, Marktoberdorf, Germany [link]
  • 090828 5pm (overview): International Summer School on Advances in Programming Languages, Heriot-Watt University, Edinburgh, UK
  • 100113 2pm (overview): Departmental Seminar, Department of Computing, Imperial College, London, UK