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
Pages73-104
Number of pages32
Volume25
ISBN (Electronic)978-1-60750-100-8
ISBN (Print)978-1-60750-099-5
DOIs
Publication statusPublished - 2010

Publication series

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

Fingerprint

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

Cite this