Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
effectcaps [2013/06/16 22:20] – ifiguero | effectcaps [2015/03/13 19:31] (current) – ifiguero | ||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Effect Capabilities ====== | + | ====== Effect Capabilities |
- | Inspired on capability-based security, we propose Effect Capabilities as an effective and flexible manner to control effects and their interferences. Capabilties can be selectively shared between modules to establish secure effect-centric coordinations. | + | |
- | ====== | + | ===== Submitted to Special Issue of Science of Computer Programming |
- | The Haskell implementation of Effect Capabilities can be downloaded {{research: | + | |
- | The code was tested in the [[http:// | + | ==== Abstract ==== |
- | + | Computational effects complicate the tasks of reasoning about and | |
- | ====== Examples ====== | + | maintaining software, due to the many kinds of interferences that |
- | Examples from the paper are included in the implementation. | + | 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 ====== | ====== Authors ====== |