page 1  (155 pages)
2to next section

We study the operational, denotational, and axiomatic semantics of lazy and call-by-value functional languages, and use these semantics to build a new expressiveness theory for comparing functional languages. The first part of the thesis develops the theory of lazy and call-by-value languages separately, following paradigmatic studies of call-by-name functional languages. We first describe the operational semantics of two simply-typed languages, lazy PCF and call-byvalue PCF. These two languages provide enough intuition to describe general definitions of denotational models and logics for lazy and call-by-value languages. We prove, via a completeness theorem, that the definitions of models and logic coincide for both the lazy and call-by-value theories. The second part of the thesis compares the two kinds of languages via translations. Specifically, we develop the idea of a fully abstract translation and define new fully abstract translations from call-by-value PCF to lazy PCF, and vice versa. We then use the ideas to develop an expressiveness theory for languages. The theory shows that call-byvalue PCF and lazy PCF are equally expressive, and another language, call-by-name PCF, is strictly less expressive than either of the other two.