Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
| effectcaps [2013/03/29 06:31] – created ifiguero | effectcaps [2015/03/13 16:31] (current) – ifiguero | ||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Effect Capabilities ====== | + | ====== Effect Capabilities |
| + | ===== Submitted to Special Issue of Science of Computer Programming ===== | ||
| + | |||
| + | ==== Abstract ==== | ||
| + | Computational effects complicate the tasks of reasoning about and | ||
| + | maintaining software, due to the many kinds of interferences that | ||
| + | can occur. While different proposals have been formulated to | ||
| + | alleviate the fragility and burden of dealing with specific effects, | ||
| + | such as state or exceptions, there is no prevalent robust mechanism | ||
| + | that addresses the general interference issue. Building upon the | ||
| + | idea of capability-based security, we propose effect capabilities as | ||
| + | an effective and flexible manner to control monadic effects and | ||
| + | their interferences. Capabilities can be selectively shared between | ||
| + | modules to establish secure effect-centric coordination. We further | ||
| + | refine capabilities with type-based permission lattices to allow | ||
| + | fine-grained decomposition of authority. We provide an | ||
| + | implementation of effect capabilities in Haskell, using type classes | ||
| + | to establish a way to statically share capabilities between modules, | ||
| + | as well as to check proper access permissions to effects at compile | ||
| + | time. We first exemplify how to tame effect interferences using | ||
| + | effect capabilities by treating state and exceptions. Then we focus | ||
| + | on taming I/O by proposing a fine-grained lattice of I/O permissions | ||
| + | based on the current classification of its operations. Finally, we | ||
| + | show that integrating effect capabilities with modern tag-based | ||
| + | monadic mechanisms provides a practical, modular and safe mechanism | ||
| + | for monadic programming in Haskell. | ||
| + | | ||
| + | ==== Implementation and Examples ==== | ||
| + | The Haskell implementation of Effect Capabilities and the examples of the paper are available in [[https:// | ||
| + | |||
| + | ====== Authors ====== | ||
| + | * Ismael Figueroa | ||
| + | * Nicolas Tabareau | ||
| + | * Éric Tanter | ||