\documentclass{ws-book9x6}

\usepackage{makeidx}

\makeindex

\usepackage[english]{babel}
\usepackage{amsmath,amssymb}

\input prooftree

\newcommand{\A}{{\mathcal{A}}}
\newcommand{\Nat}{{\mathbb{N}}}
\newcommand{\ze}{{\mathsf{zero}}}
\newcommand{\su}{{\mathsf{succ}}}
\newcommand{\pr}{{\mathsf{pred}}}
\newcommand{\ifz}{{\mathsf{ifz}}}
\newcommand{\cond}{{\mathsf{cond}}}
\newcommand{\pcond}{{\mathsf{pcond}}}
\newcommand{\arr}{\rightarrow}
\newcommand{\wenn}{{\mathbf{if}}}
\newcommand{\dann}{{\mathbf{then}}}
\newcommand{\sonst}{{\mathbf{else}}}
\newcommand{\nnew}{{\mathbf{fi}}}
\newcommand{\ifte}[3]{\wenn \, #1 \, \dann \,#2 \, \sonst \, #3 \, \nnew}
\newcommand{\pif}[3]{\mathbf{pif} \,#1\, \dann \,#2\, \sonst \,#3\, 
                     \mathbf{fip}}
\newcommand{\PCF}{{\mathrm{PCF}}}
\newcommand{\LCF}{{\mathrm{LCF}}}
\newcommand{\evto}{{\Downarrow}}
\newcommand{\nat}{{\mathbf{nat}}}
\newcommand{\bool}{{\mathbf{bool}}}
\newcommand{\por}{{\mathsf{por}}}
\newcommand{\pand}{{\mathsf{pand}}}
\newcommand{\portest}{{\mathsf{portest}}}
\newcommand{\Type}{{\mathsf{Type}}}
\newcommand{\true}{{\mathsf{true}}}
\newcommand{\false}{{\mathsf{false}}}
\newcommand{\ev}{{\mathsf{ev}}}
\newcommand{\App}{{\mathsf{App}}}
\newcommand{\Y}{{\mathsf{Y}}}
\newcommand{\red}{\vartriangleright}
\newcommand{\Prg}{{\mathsf{Prg}}}
\newcommand{\bisleq}{\stackrel{\sqsubset}{_\sim}}
\newcommand{\obsleq}{\stackrel{<}{_\sim}}
\newcommand{\sto}{{\mathsf{stop}}}
\newcommand{\ar}{{\mathsf{arg}}}
\newcommand{\dom}{{\mathsf{dom}}}
\newcommand{\pair}[2]{\langle #1 , #2 \rangle}
\newcommand{\id}{{\mathsf{id}}}
\newcommand{\Pow}{{\mathcal{P}}}
\newcommand{\glb}{{\mathsf{glb}}}
\newcommand{\dotminus}{\stackrel{.}{-}}
\newcommand{\less}{{\mathsf{less}}}
\newcommand{\strarr}{\mbox{$\circ \kern-0.4em \arr$}}
\newcommand{\parr}{\rightharpoonup}
\newcommand{\C}{{\mathcal C}}
\newcommand{\op}{{\mathsf op}}
\newcommand{\SFP}{{\mathrm{SFP}}}
\newcommand{\fix}{{\mathsf{fix}}}
\newcommand{\SD}{{\mathcal{S}}}
\newcommand{\pPart}{{\mathsf{pPart}}}
\newcommand{\SSP}{{\mathbf{SSP}}}
\newcommand{\restrict}{{\upharpoonright}}
\newcommand{\one}{{\mathrm{1}}}
\newcommand{\subtrunc}{\ensuremath{\makebox[.25em][l]{$-$}\raisebox{1ex}{.}\;}}
\newcommand{\CE}{\mathcal{K}}
\newcommand{\epsi}{{\varepsilon}}
\newcommand{\egDom}{{\mathsf{Dom_{eff}}}}
\newcommand{\Comp}{{\mathsf{Comp}}}
\newcommand{\EN}{{\mathsf{EN}}}
\newcommand{\fst}{\mathrm{fst}}
\newcommand{\snd}{\mathrm{snd}}
\newcommand{\size}{\mathrm{size}}
\newcommand{\search}{\mathrm{search}}
\newcommand{\Or}{\mathrm{Or}}
\newcommand{\join}{\mathrm{join}}
\newcommand{\enum}{\mathrm{enum}}
\newcommand{\sjoin}{\mathrm{sjoin}}
\newcommand{\up}{\mathrm{up}}
\newcommand{\below}{\mathrm{below}}
\newcommand{\paar}[2]{\langle #1 , #2 \rangle}


\newcommand{\encode}[1]{\mathopen{{}^\ulcorner\mkern-2mu} #1
  \mathclose{\mkern-1mu{}^\urcorner}} % needs amssymb.sty

\def\lbr{\mathopen{{[\kern-0.14em[}}}   % opening [[ value delimiter
\def\rbr{\mathclose{{]\kern-0.14em]}}}  % closing ]] value delimiter
\newcommand{\sem}[1]{\lbr#1\rbr}
\newcommand{\MYenddef}{\hfill\mbox{$\lozenge$}}

\newtheorem{dfn}{Definition}[chapter]
\newtheorem{lem}[dfn]{Lemma}
\newtheorem{cor}[dfn]{Corollary}
\newtheorem{theo}[dfn]{Theorem}
\newtheorem{exa}[dfn]{Example}
%%Proof Environment
%\newenvironment{proof}{\noindent{\em Proof:}}
%               {\nopagebreak\hfill$\Box$\vspace{2ex}}

% Diagrams

\input{diagrams}
%\diagramstyle[PostScript=dvips]

\newarrow{Dashto}{}{dash}{}{dash}>
\newarrow{Embed}>--->
\newarrow{Into} C--->
\newarrow{To} ---->
\newarrow{Line} -----
\newarrow{Onto} ----{>>}

\begin{document}

%%%%%%%%%%%%%% Please do not remove these lines %%%%%%%%%%%%%%%%%%%%%
\titlepages %pls. leave this as it is. 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%% GENERATE OUT THE TOC FILE %%%%%%%%%%%%%%%%%%%%%
\begin{tblofcontents}
%%%%% Need not to input any data here. 
%%%%% System will input automatically.
\end{tblofcontents}
%%%%%%%%%%%%%%%%%%%% GENERATE OUT THE TOC FILE %%%%%%%%%%%%%%%%%%%%%

%% Don't know how to set the title (cf. ws-book9x6.tex)
%% No instructions given. No Example given either.
%\title{Denotational Foundations of \\ Functional Programming }
%\author{Thomas Streicher}
%\date{SS 04} 
%\maketitle

\begin{dedication}
dedicated to Dana Scott and Gordon Plotkin \\ who invented domain theory and
logical relations
%\large Dedication Page \\[13pt]
%\large (optional)
\end{dedication}

\begin{preface}
\input{preface}
\end{preface}

\setcounter{page}{0}

\input{intro}
\input{mgfp1}\input{mgfp2}\input{mgfp3}\input{mgfp4}\input{mgfp5}
\input{mgfp6}\input{mgfp7}\input{mgfp8}\input{mgfp9}\input{mgfp10}
\input{mgfp11}\input{mgfp12}

\newpage
\begin{thebibliography}{Be792}
\bibitem[Abramsky et.al.\ 2000]{AJM} S.~Abramsky, R.~Jagadeesan, P.~Malacaria 
\newblock \emph{Full Abstraction for $\PCF$} 
\newblock Inform.~and Comput.~163, no.~2, 409--470 (2000).
\bibitem[Amadio and Curien 1998]{AC} R.~Amadio and P.-L.~Curien
\newblock {\em Domains and $\lambda$-Calculi.} 
\newblock Cambridge Univ.\ Press (1998).
\bibitem[Asperti 1990]{Asp} A.~Asperti
\newblock {\em Stability and computability in coherent domains.} 
\newblock Inform.~and Comput.~86, no.~2, 115-139 (1990).
\bibitem[Barendregt 1981]{Bar} H.~Barendregt
\newblock \emph{The Lambda Calculus. Its Syntax and Semantics.}
\newblock North Holland (1981).
\bibitem[Barr and Wells 1990]{BW} M.~Barr and Ch.~Wells
\newblock \emph{Category theory for computing science.}
\newblock Prentice Hall International (1990).
\bibitem[Berry 1979]{Be1} G.~Berry
\newblock \emph{Mod\`eles compl\`etement ad\'equats et stables des
                lambda calculs typ\'es}
\newblock Th\'ese d' Etat, Universit\'e Paris 7 (1979).
\bibitem[Escard\'o 1997]{EscPhD} M.~H.~Escard\'o
\newblock \emph{$\PCF$ extended with real numbers: a domain-theoretic approach
                to higher-order exact real number computation.}
\newblock PhD Thesis, Imperial College, Univ.~of London (1997).
\bibitem[Griffor et.al.\ 1994]{GLS} 
        E.~Griffor, I.~Lindstr\"om and V.~Stoltenberg-Hansen
\newblock {\em Mathematical Theory of Domains.} 
\newblock Cambridge Univ.\ Press (1994).
\bibitem[Hyland 1990]{Hy} J.~M.~E.~Hyland
\newblock \emph{First steps in synthetic domain theory.}
\newblock  in \emph{Category Theory (Como 1990)} pp.131--156,
\newblock  Lecture Notes in Math.\ 1488 Springer, Berlin, 1991.
\bibitem[Hyland and Ong 2000]{HO} M.~Hyland, L.~Ong
\newblock \emph{On Full Abstraction for $\PCF$: I,II and III.} 
\newblock Inform.~and Comput.~163, no. 2, pp.285--408 (2000).
\bibitem[Kanda and Park 1979]{KP} A.~Kanda, D.~Park
\newblock \emph{When are two effectively given domains identical?}
\newblock pp. 563--577, LNCS 67, Springer, Berlin-New York, 1979. 
\bibitem[Liguoro 1996]{Lig} U.~de'Liguoro
\newblock \emph{PCF definability via Kripke logical relations (after O'Hearn
and Riecke)}
\newblock Lab.~Inf.~ENS, Report LIENS-96-7, Paris (1996).
\bibitem[Loader 2001]{Loa} R.~Loader
\newblock \emph{Finitary PCF is not decidable} 
\newblock TCS 266, no.~1-2, pp.~341-364 (2001).
\bibitem[Longley 2002]{Lon} J.~Longley
\newblock \emph{Sequentially Realizable Functionals} 
\newblock APAL 117, no.~1-3, pp.~1-93 (2002).
\bibitem[MacLane 1998]{McL} S.~MacLane
\newblock \emph{Categories for the Working Mathematician}
\newblock Second edition. Graduate Texts in Mathematics 5, Springer (1998).
\bibitem[Marz 2000]{Mar} M.~Marz
\newblock \emph{A Fully Abstract Model for Sequential Computation}
\newblock  PhD Thesis, TU Darmstadt (2000) electronically available from \\
\newblock $\mathtt{www.mathematik.tu}$-$\mathtt{darmstadt.de/\,\tilde{}\,
           streicher/THESES/marz.ps.gz}$
\bibitem[McCusker 1998]{McC} G.~McCusker
\newblock \emph{Games and full abstraction for a functional metalanguage
                with recursive types.}
\newblock CPHC/BCS Distinguished Dissertations, Springer Verlag London (1998).
\bibitem[Milner 1977]{Mil} R.~Milner
\newblock \emph{Fully Abstract Models of Typed $\lambda$-Calculi}
\newblock TCS 4, pp.~1-22 (1977).
\bibitem[Normann 2006]{Nor} D.~Normann
\newblock \emph{On sequential functionals of type $3$}
\newblock to appear in Math.~Struct.~Comput.~Sc.\ as part of a
          Festschrift for K.~Keimel (2006).
\bibitem[Plotkin 1977]{Pl77} G.~Plotkin
\newblock \emph{LCF considered as a programming language}
\newblock TCS 5, pp.~223-255 (1977).
\bibitem[Plotkin 1978]{Pl78} G.~Plotkin
\newblock \emph{$\mathbb{T}^\omega$ as a universal domain}
\newblock J.~Comput.~System~Sci.~17 (1978), no. 2, 209--236.
\bibitem[O'Hearn and Riecke 1995]{OR} P.~O'Hearn, J.~Riecke
\newblock \emph{Kripke logical relations and PCF}
\newblock Inf.~and Comp.~120, no.~1, pp.~107-116 (1995).
\bibitem[Reus and Streicher 1999]{ReSt} B.~Reus, T.~Streicher
\newblock \emph{General synthetic domain theory---a logical approach.}
\newblock  Math.~Structures Comput.~Sci.~9, no.~2, pp.~177--223 (1999). 
\bibitem[Riecke and Sandholm 2002]{RS} J.~Riecke, A.~Sandholm
\newblock \emph{A relational account of call-by-value sequentiality}
\newblock Inf.~and Comp.~179, no.~2, pp.~296-331 (2002).
\bibitem[Rogers 1987]{Ro} H.~Rogers jr.
\newblock \emph{Theory of recursive functions and effective computability.}
\newblock 2$^{\mathrm{nd}}$ edition, MIT Press, Cambridge, MA, 1987.
\bibitem[Rohr 2002]{Roh} A.~Rohr
\newblock \emph{A Universal Realizability Model for Sequential Computation.}
\newblock  PhD Thesis, TU Darmstadt (2002) electronically available from \\
\newblock $\mathtt{www.mathematik.tu}$-$\mathtt{darmstadt.de/\,\tilde{}\,
           streicher/THESES/rohr.ps.gz}$ 
\bibitem[Scott 1969]{Sc1} Dana S.~Scott
\newblock \emph{A type-theoretical alternative to ISWIM, CUCH, OWHY}
\newblock unpublished paper from 1969 reprinted in 
\newblock \emph{B\"ohm Festschrift} TCS 121 No.1-2, pp.~411-440 (1993).
\bibitem[Scott 1980]{Sc2} Dana S.~Scott
\newblock \emph{Relating theories of the $\lambda$-calculus}
\newblock in \emph{To H. B. Curry: essays on combinatory logic, lambda 
calculus and formalism} pp.~403-450 Academic Press, London-New York (1980).
\bibitem[Sieber 1992]{Sie} K.~Sieber
\newblock \emph{Reasoning about sequential functions via logical relations}
\newblock in \emph{Applications of category theory in computer science} 
          pp.258--269
\newblock  London Math.\ Soc.\ Lecture Note Ser., 177, CUP (1992).
\bibitem[Simpson 2004]{Sim} A.~Simpson
\newblock \emph{Computational Adequacy for Recursive Types 
                in Models of Intuitionistic Set Theory.}
\newblock Ann.~Pure Appl.~Logic 130,  no.\ 1-3, pp.~207--275 (2004).
\bibitem[Stoughton 1990]{Sto} A.~Stoughton
\newblock \emph{Equationally fully abstract models of $\PCF$}
\newblock Proc.~of \emph{Fifth International Conference on the
          Mathematical Foundations of Computer Science}
\newblock Springer Lecture Notes in Comput.~Sci.~442, pp.271--283 (1990)
\bibitem[Streicher 1994]{St94} T.~Streicher
\newblock \emph{A universality theorem for $\PCF$ with recursive types,
                parallel-or and $\exists$.}
\newblock Math.~Struct.~Comput.~Sc.~4, no.~1, pp.111-115 (1994).
\bibitem[Streicher and Reus 1998]{SR} T.~Streicher, B.~Reus
\newblock \emph{Classical logic, continuation semantics and abstract machines.}
\newblock J.~Funct.~Programming 8 (1998), no.~6, 543--572. 
\bibitem[Taylor 1991]{Ta} P.~Taylor
\newblock \emph{The fixed point property in synthetic domain theory.}
\newblock in \emph{Proc.\ 6th IEEE Symposium on Logic in Computer Science},
          pp.152-160 (1991).
\bibitem[Winskel 1993]{Win} G.~Winskel
\newblock \emph{The formal semantics of programming languages. An introduction.}
\newblock MIT Press, Cambridge MA (1993).

\end{thebibliography}

\printindex

\end{document}
