An Operational Logic of Effects

Ian A. Mason
Applied Computing & Mathematics University of Tasmania @ Launceston Launceston, Tasmania 7250 Australia.
imason@leven.appcomp.utas.edu.au

Jacob Frost
Computer Laboratory University of Cambridge New Museums Site Pembroke Street Cambridge CB2 3QG England.
Jacob.Frost@cl.cam.ac.uk

Abstract

In this paper we describe our progress towards an operational implementation of a modern programming logic. The logic is inspired by the variable type systems of Feferman, and is designed for reasoning about imperative functional programs. The logic goes well beyond traditional programming logics, such as Hoare's logic and Dynamic logic in its expressibility, yet is less problematic to encode into higher-order logics. The main focus of the paper is too present an axiomatization of the base first-order theory, and an implementation of the logic into the generic proof assistant Isabelle. We also indicate the directions of our current research to blend these two advances into an operational whole.

Conference Home Page