Lightweight Static Capabilities

Oleg Kiselyov, Chung chieh Shan

Research output: Contribution to journalArticlepeer-review

9 Citations (Scopus)

Abstract

We describe a modular programming style that harnesses modern type systems to verify safety conditions in practical systems. This style has three ingredients:(i)A compact kernel of trust that is specific to the problem domain.(ii)Unique names (capabilities) that confer rights and certify properties, so as to extend the trust from the kernel to the rest of the application.(iii)Static (type) proxies for dynamic values. We illustrate our approach using examples from the dependent-type literature, but our programs are written in Haskell and OCaml today, so our techniques are compatible with imperative code, native mutable arrays, and general recursion. The three ingredients of this programming style call for (1) an expressive core language, (2) higher-rank polymorphism, and (3) phantom types.

Original languageEnglish
Pages (from-to)79-104
Number of pages26
JournalElectronic Notes in Theoretical Computer Science
Volume174
Issue number7
DOIs
Publication statusPublished - 2007 Jun 4

Keywords

  • Modular programming
  • safety property
  • static types
  • verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Lightweight Static Capabilities'. Together they form a unique fingerprint.

Cite this