\relax 
\citation{abadi97calculus}
\citation{Blanchet:ProVerif}
\citation{Blanchet:ProVerif}
\@writefile{toc}{\contentsline {section}{\numberline {1}Syntax of the Core Calculus}{1}}
\newlabel{sec:syntax:core}{{1}{1}}
\citation{JGL:eva:sem}
\citation{NNS:H1}
\@writefile{toc}{\contentsline {section}{\numberline {2}Approximating Equality}{4}}
\newlabel{sec:eq}{{2}{4}}
\citation{JGL-ipl2005}
\citation{CS:MACE}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Finding an over-approximation of equality}{5}}
\newlabel{sec:eq:eq}{{2.1}{5}}
\citation{JGL:JFLA04}
\newlabel{eq:approxE}{{5}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Finding an over-approximation of disequality}{7}}
\newlabel{sec:eq:neq}{{2.2}{7}}
\citation{abadi97calculus}
\citation{NNS:H1}
\@writefile{toc}{\contentsline {section}{\numberline {3}The Semantics of the Core Calculus}{10}}
\newlabel{sec:sem}{{3}{10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}The Lean Semantics}{10}}
\newlabel{sec:sem:lean}{{3.1}{10}}
\citation{Blanchet:prolog}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}The Light Semantics}{14}}
\newlabel{sec:sem:light}{{3.2}{14}}
\@writefile{toc}{\contentsline {section}{\numberline {4}The Full Language}{20}}
\newlabel{sec:full}{{4}{20}}
\bibstyle{apalike}
\bibdata{ispi}
\bibcite{abadi97calculus}{{1}{1997}{{Abadi and Gordon}}{{}}}
\bibcite{Blanchet:prolog}{{2}{2001}{{Blanchet}}{{}}}
\bibcite{Blanchet:ProVerif}{{3}{2004}{{Blanchet}}{{}}}
\bibcite{CS:MACE}{{4}{2003}{{Claessen and S{\"o}rensson}}{{}}}
\bibcite{JGL:eva:sem}{{5}{2001}{{Goubault-Larrecq}}{{}}}
\bibcite{JGL:JFLA04}{{6}{2004}{{Goubault-Larrecq}}{{}}}
\bibcite{JGL-ipl2005}{{7}{2005}{{Goubault{-}Larrecq}}{{}}}
\bibcite{NNS:H1}{{8}{2002}{{Nielson et~al.}}{{}}}