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.