@techreport{gordon2009principles,
author = {Gordon, Andy and Fournet, Cédric},
title = {Principles and Applications of Refinement Types},
year = {2009},
month = {October},
abstract = {A refinement type x:T|C is the subset of the type T consisting of the values x to satisfy the formula C. In these tutorial notes we explain the principles of refinement types by developing from first principles a concurrent lambda-calculus whose type system supports refinement types. Moreover, we describe a series of applications of our refined type theory and of related systems.},
url = {http://approjects.co.za/?big=en-us/research/publication/principles-and-applications-of-refinement-types/},
number = {MSR-TR-2009-147},
}