Computational e!ects, algebraic theories and normalization by evaluation
Danel Ahman, Hughes Hall · 2012
This dissertation is concerned with modeling and reasoning about impure ML-like higherorder programs. Our work is based on the algebraic theories of computational effects 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 extensive work. Before one is able to correctly reason about the terms in the value and effect theories and the corresponding terms in the intermediate language, it is necessary to effectively decide provable equality in the intermediate language. As a result, we spend a significant proportion of this dissertation on developing a suitable normalization by evaluation (NBE) algorithm to compute canonical normal forms in the intermediate language. The comparison of these normal forms provides us with the necessary decision procedure for proving the conservativity theorem. The NBE algorithm we define is a generalization of the usual presentations of NBE 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 formalized the syntax of the intermediate language together with the formally verified NBE algorithm in the interactive theorem prover and functional programming language Agda.