1 citations · 1 across the 5 of their papers we have counts for
5 papers · 1 filter
Semantically Separating Nominal Wyvern for Usability and Decidability
Yu Xiang Zhu, Amos Robinson, Sophia Roshal +4
The Dependent Object Types (DOT) calculus incorporates concepts from functional languages (e.g. modules) with traditional object-oriented features (e.g. objects, subtyping) to achi…
Reasoning about External Calls
Sophia Drossopoulou, Julian Mackay, Susan Eisenbach +1
In today's complex software, internal trusted code is tightly intertwined with external untrusted code. To reason about internal code, programmers must reason about the potential e…
Necessity Specifications for Robustness
Julian Mackay, Sophia Drossopoulou, James Noble +1
Robust modules guarantee to do only what they are supposed to do - even in the presence of untrusted, malicious clients, and considering not just the direct behaviour of individual…
Rusty Links in Local Chains
James Noble, Julian Mackay, Tobias Wrigstad
Rust successfully applies ownership types to control memory allocation. This restricts the programs' topologies to the point where doubly-linked lists cannot be programmed in Safe…
Holistic Specifications for Robust Programs
Sophia Drossopoulou, James Noble, Julian Mackay +1
Functional specifications describe what program components do: the sufficient conditions to invoke a component's operations. They allow us to reason about the use of components in…