Computer Laboratory
University of Cambridge
Thursday, 5 July 2011, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: We investigate the use of universal algebra for modeling impure ML-like higher-order programs. We have based our work on the algebraic theories of computational effects first proposed by Plotkin and Power. In particular, we present an extension from the algebraic value and effect theories to a fine-grained call-by-value intermediate language. Whilst this extension has a straightforward definition and is intuitively correct, the proof of its conservativeness requires one to effectively decide provable equality in the intermediate language. As a result, we define a suitable semantic reduction-free normalization algorithm, called normalization by evaluation, to compute normal forms whose comparison provides us with the necessary decision procedure for proving the conservativity theorem.
The normalization by evaluation algorithm we define is a generalization of the usual presentations of normalization by evaluation where normal forms are identified up to equality rather than modulo the given value and effect theories. However, the usual normalization results arise as special cases when the value and effect theories do not contain equations. We have also implemented and formally verified the normalization by evaluation algorithm in Agda.
In this talk I will discuss the value and effect theories proposed by Plotkin and Pretnar, show the extension of these theories to the intermediate language and describe our normalization by evaluation algorithm together with its use in proving the conservativity theorem.