Skip to main content Skip to navigation


This page has no content yet.

  • Combinatorial reasoning in Information Theory
    Noga Alon, Tel Aviv University
    Combinatorial arguments have played a crucial role in the investigation of several surprising phenomena in Information Theory. After a brief discussion of some of these results I will describe a recent example, based on joint papers with Lubetzky and Stav, and with Hassidim and Weinstein, in which properties of graph powers, colorings of Cayley graphs, and the chromatic numbers of Kneser graphs are applied in the study of a broadcasting problem with side information.
  • Lectures on Principles and Applications of Refinement Types
    Andy Gordon, MSR Cambridge
    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.