Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Principles and Applications of Refinement Types

Andrew D. Gordon and C├ędric Fournet

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.

Details

Publication typeTechReport
NumberMSR-TR-2009-147
> Publications > Principles and Applications of Refinement Types