## Computational effects, algebraic theories and normalization by evaluation

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.

Tarmo Uustalu

Last update 22.6.2012