4 citations · 7 across the 8 of their papers we have counts for
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…
Sound Invariant Checking Using Type Modifiers and Object Capabilities
Isaac Oscar Gariano, Marco Servetto, Alex Potanin
In this paper we use pre existing language support for type modifiers and object capabilities to enable a system for sound runtime verification of invariants. Our system guarantees…
Iteratively Composing Statically Verified Traits
Isaac Oscar Gariano, Marco Servetto, Alex Potanin +1
Static verification relying on an automated theorem prover can be very slow and brittle: since static verification is undecidable, correct code may not pass a particular static ver…