Lightweight Static Capabilities

Oleg Kiselyov, Chung chieh Shan

研究成果: Article査読

9 被引用数 (Scopus)

抄録

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.

本文言語English
ページ(範囲)79-104
ページ数26
ジャーナルElectronic Notes in Theoretical Computer Science
174
7
DOI
出版ステータスPublished - 2007 6 4

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント 「Lightweight Static Capabilities」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル