Principles and Applications of Refinement Types

Andrew D. Gordon, Cédric Fournet

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationLogics and Languages for Reliability and Security
PublisherIOS Press
Number of pages32
ISBN (Electronic)978-1-60750-100-8
ISBN (Print)978-1-60750-099-5
Publication statusPublished - 2010

Publication series

NameNATO Science for Peace and Security Series - D: Information and Communication Security
PublisherIOS Press
ISSN (Print)1874-6268
ISSN (Electronic)1879-8292


Dive into the research topics of 'Principles and Applications of Refinement Types'. Together they form a unique fingerprint.

Cite this