ETD

• algebraic effect handlers
• algebraic effects
• program verification
• runtime verification
• temporal logics

Runtime Verification has proved to be a valuable, lightweight tool to formally verify program properties. However, runtimes themselves has been evolving, with new ways to reason about programs and new ways to encode behaviours. Together with these new features, inevitably come new bugs and new security flaws, but also new ways to counteract them. In this thesis, we develop a framework to perform Runtime Verification of a language with Algebraic Effect Handlers, with the aim of providing a convenient way of verifying properties on the effects produced by a computation, and enabling compositional reasoning on them, with the ultimate goal of writing safe and secure software. To specify security properties, we provide a temporal logic that is able to reason on the invocation of operations, then show how to translate a generic formula to a monitor, and ultimately how to instrument a program with this monitor to ensure that we can detect and act when the program violates the specified property.