Denotational semantics and proof methods for a lazy functional language

Formal description of a language gives insight into the language itself. The formal description may point out inconsistencies in the language, result in new program constructions or/and deliver useful proof methods. The formal description can be divided into the structure or syntax of programs in the language and semantics or meaning of programs.The semantics of a language can be described in many ways. An operational semantics describes the meaning or behavior of a program by means of (operational) arguments based on the execution of the program. A denotational semantics models the program as a mathematical object in a domain of possible meanings. This object can then be understood by mathematical tools and rules. There are more semantic models and the relations between these models have been studied by many people.A model is fully abstract when all the objects in the model correspond to programs in the language. Proving such is quite intricate. A good overview of the current status of the research into denotational semantics and the problem of full abstractness can be found in [Jun96]. In this paper we shall concentrate on the denotational semantics of a functional language. From the mathematics of the semantics we will gain insight into some proof methods which are connected to a denotational semantics. Chapter 2 is a quick introduction to domain theory. The necessary mathematical constructions for specifying a denotational semantics is presented. The chapter is based on chapters 8 and 12 of [Win92], and the omitted proofs can be found there.Chapter 3 presents the language Lapa which was the starting point for our paper. In this chapter we define the characteristics of Lapa and try to formalize a denotational semantics. The chapter concludes with the deficiencies of Lapa and their solutions. Chapter 4 presents the language Lager which is a possible language one might acquire if the deficiencies of Lapa are solved. The formal definition of Lager including an operational and a denotational semantics are presented here. Chapter 5 reviews some proof methods. The soundness of the proof principle for properties of infinite, partial and finite lists found in chapter 9 of [Bir98J is investigated. The approximation lemma which can also be found in chapter 9 of [Bir98] is also looked into. The chapter concludes with a brief remark on other proof methods. It is largely a brief summary of the article [GH99]. Chapter 6 presents some conclusions and points out further work.Appendix A gives an implementation of Lager in Haskell based on monads. Roughly the same implementation in Gofer without monads can be found in Appendix B.