@inproceedings{533d163f04be46249331486c1836f615,
title = "Capabilities: Effects for Free",
abstract = "Object capabilities are increasingly used to reason informally about the properties of secure systems. But can capabilities also aid in formal reasoning? To answer this question, we examine a calculus that uses effects to capture resource use and extend it to support capability-based reasoning. We demonstrate that capabilities provide a way to reason about effects: we can bound the effects of an expression based on the capabilities to which it has access. This reasoning is “free” in that it relies only on type-checking (not effect-checking), does not require the programmer to add effect annotations within the expression, and does not require the expression to be analysed for its effects. Our result sheds light on the essence of what capabilities provide and suggests ways of integrating lightweight capability-based reasoning into languages.",
author = "Aaron Craig and Alex Potanin and Lindsay Groves and Jonathan Aldrich",
note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2018.; 20th International Conference on Formal Engineering Methods, ICFEM 2018 ; Conference date: 12-11-2018 Through 16-11-2018",
year = "2018",
doi = "10.1007/978-3-030-02450-5\_14",
language = "English",
isbn = "978-3-030-02449-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "231--247",
editor = "Jing Sun and Meng Sun",
booktitle = "Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Proceedings",
address = "Germany",
}