8 papers
More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme
James Noble, David Streader, Isaac Oscar Gariano +1
Formal methods for software correctness are critical to the future of software engineering - and so must be an essential part of software engineering education. Unfortunately, form…
Dala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom
Kiko Fernandez-Reyes, Isaac Oscar Gariano, James Noble +3
Dynamic languages like Erlang, Clojure, JavaScript, and E adopted data-race freedom by design. To enforce data-race freedom, these languages either deep copy objects during actor (…
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…
Mμl: The Power of Dynamic Multi-Methods
Isaac Oscar Gariano, Marco Servetto
Multi-methods are a straightforward extension of traditional (single) dynamic dispatch, which is the core of most object oriented languages. With multi-methods, a method call will…
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…