Principles and Applications of Refinement Types
Andrew D. Gordon, Fournet Cédric · NATO science for peace and security series. D, Information and communication security · 2010
A refinement type {x : T | C} is the subset of the type T consisting of the values x to satisfy the formula C. In this tutorial article we explain the principles of refinement types by developing from first principles a concurrent λ-calculus whose type system supports refinement types. Moreover, we describe a series of applications of our refined type theory and of related systems.