5 papers
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…
Towards Gradual Checking of Reference Capabilities
Kiko Fernandez-Reyes, Isaac Oscar Gariano, James Noble +1
Concurrent and parallel programming is difficult due to the presence of memory side-effects, which may introduce data races. Type qualifiers, such as reference capabilities, can re…
Which of My Transient Type Checks Are Not (Almost) Free?
Isaac Oscar Gariano, Richard Roberts, Stefan Marr +2
One form of type checking used in gradually typed language is transient type checking: whenever an object 'flows' through code with a type annotation, the object is dynamically che…
CallE: An Effect System for Method Calls
Isaac Oscar Gariano, James Noble, Marco Servetto
Effect systems are used to statically reason about the effects an expression may have when evaluated. In the literature, such effects include various behaviours as diverse as memor…
Transient Typechecks are (Almost) Free
Richard Roberts, Stefan Marr, Michael Homer +1
Transient gradual typing imposes run-time type tests that typically cause a linear slowdown in programs' performance. This performance impact discourages the use of type annotation…