A typed functional programming language, called PCF, is presented in this thesis together with its type checking rules, substitution rules and its operational semantics. The safety theorem is proven. It is shown that recursion is a fixed point. Domains, which are motivated by an attempt of implementing naive semantics, are presented. It is shown that every continuous function has the least fixed point and some of the continuous functions between domains are presented. A function that assigns to a continuous function its least fixed point is defined. Denotational semantics using domains is implemented. Substitution lemma and correctness theorem are proven, and soundness theorem is proved using logical relations. Computational adequacy is at the end shown as a consequence of correctness and soundness theorems.
|
