BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Principles and applications of refinement types - Andy Gordon (Mic
 rosoft Research)
DTSTART:20090701T123000Z
DTEND:20090701T133000Z
UID:TALK18597@talks.cam.ac.uk
CONTACT:Dr Fabien Petitcolas
DESCRIPTION:*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 i
 dea has been known in the research community for some time\, it has been a
 ssumed impractical\, because of the difficulties of constraint solving. Bu
 t recent advances in automated reasoning have overturned this conventional
  wisdom\, and transformed the idea into a practical design principle. I wi
 ll present a primer on the design\, implementation\, and application of re
 finement types. I will explain:\n\n* How a range of diverse features may b
 e unified as instances of the general idea of refinement types.\n* How a s
 tatic checker for the Oslo modeling language M allows us to check for secu
 rity errors in server configurations\; intended constraints on configurati
 ons are expressed with refinement types\, so that configuration validation
  reduces to type checking.\n* How we statically check integrity and secrec
 y 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.\n\n*Biography*: Andy Gordon is a Principal Researc
 her at MSR Cambridge. His research interests are in the general area of pr
 ogramming languages. His work at Microsoft has involved applying type theo
 ry and other formal techniques to problems of computer security. His proje
 cts include the following: an analysis (with D. Syme) of the type system u
 nderlying the bytecode verifier of the Microsoft .NET Common Language Runt
 ime\; Cryptyc (with A. Jeffrey)\, a type-checker for cryptographic protoco
 ls\; and the Samoa Project (with K. Bhargavan and C. Fournet) on formal to
 ols for the security of XML Web Services. He is currently excited about th
 e many possibilities of refinement types\, and is actively developing them
  in the context of both F# and the Oslo Modeling Language M.
LOCATION:Large public lecture room\, Microsoft Research\, Roger Needham Bu
 ilding\, 7 J J Thomson Avenue\, Cambridge CB3 0FB
END:VEVENT
END:VCALENDAR