\relax 
\bibstyle{plain}
\citation{Tait67}
\citation{Girard71}
\citation{Gallier90}
\citation{BarBer96a,Parigot00}
\citation{Krivine04}
\citation{Krivine11,Krivine12,Krivine14}
\citation{Miquel11}
\citation{GuiMiq16,GuiM16}
\@writefile{toc}{\contentsline {title}{Realizability Interpretation And Normalization Of Typed Call-by-Need $\lambda $-calculus With Control}{1}}
\@writefile{toc}{\authcount {2}}
\@writefile{toc}{\contentsline {author}{\'Etienne Miquey\unskip {} \and Hugo Herbelin\unskip {}}{1}}
\citation{Krivine03}
\citation{Herbelin12}
\citation{AriDowHerNakSau12}
\citation{CurHer00,HerbelinHdR,Munch09}
\citation{AriDowHerNakSau12}
\citation{Polonowski04}
\citation{Herbelin12}
\citation{Plotkin75}
\citation{AriFel93}
\citation{MarOdeWad98}
\citation{OkaLeeTar94}
\citation{AriDowHerNakSau12}
\citation{FelFriKohDub86}
\citation{Parigot91}
\citation{Crolard99}
\citation{CurHer00,HerbelinHdR}
\citation{LafReuStr93}
\citation{AriDowHerNakSau12}
\citation{AriDowHerNakSau12}
\citation{OkaLeeTar94}
\citation{AriDowHerNakSau12}
\@writefile{toc}{\contentsline {section}{\numberline {1}The {\relax {$\overline  {\lambda }_{[\lowercase {lv}\tau \star ]}$}}-calculus}{3}}
\newlabel{s:lbvtstar}{{1}{3}}
\newlabel{s:lbvtstar@cref}{{[section][1][]1}{3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}The call-by-need evaluation strategy}{3}}
\citation{Lang07}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Explicit environments}{4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3}Syntax \& reduction rules}{4}}
\newlabel{sec:syntax}{{1.3}{4}}
\newlabel{sec:syntax@cref}{{[subsection][3][1]1.3}{4}}
\citation{AriDowHerNakSau12}
\citation{AriDowHerNakSau12}
\citation{AriDowHerNakSau12}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Syntax and reduction rules of the $\relax {$\overline  {\lambda }_{[\lowercase {lv}\tau \star ]}$}$-calculus}}{5}}
\newlabel{fig:reduction-rules}{{1}{5}}
\newlabel{fig:reduction-rules@cref}{{[figure][1][]1}{5}}
\citation{Krivine04}
\citation{Krivine93}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Typing rules of the $\relax {$\overline  {\lambda }_{[\lowercase {lv}\tau \star ]}$}$-calculus}}{6}}
\newlabel{fig:typing-rules}{{2}{6}}
\newlabel{fig:typing-rules@cref}{{[figure][2][]2}{6}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4}A type system for the $\relax {$\overline  {\lambda }_{[\lowercase {lv}\tau \star ]}$}$-calculus.}{6}}
\newlabel{sec:typing}{{1.4}{6}}
\newlabel{sec:typing@cref}{{[subsection][4][1]1.4}{6}}
\newlabel{thm:subject}{{1}{6}}
\newlabel{thm:subject@cref}{{[theorem][1][1]1}{6}}
\citation{DagSch15}
\@writefile{toc}{\contentsline {section}{\numberline {2}Normalization of the {\relax {$\overline  {\lambda }_{[\lowercase {lv}\tau \star ]}$}}-calculus}{7}}
\newlabel{s:real}{{2}{7}}
\newlabel{s:real@cref}{{[section][2][]2}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Normalization by realizability}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Realizability interpretation for the $\relax {$\overline  {\lambda }_{[\lowercase {lv}\tau \star ]}$}$-calculus}{7}}
\newlabel{lm:st_union}{{4}{8}}
\newlabel{lm:st_union@cref}{{[lemma][4][]4}{8}}
\citation{Krivine11}
\newlabel{prop:norm_pole}{{7}{9}}
\newlabel{prop:norm_pole@cref}{{[proposition][7][]7}{9}}
\citation{AriDowHerNakSau12}
\newlabel{def:realizers}{{10}{10}}
\newlabel{def:realizers@cref}{{[definition][10][]10}{10}}
\newlabel{prop:monotonicity}{{12}{10}}
\newlabel{prop:monotonicity@cref}{{[proposition][12][]12}{10}}
\newlabel{def:store_real}{{13}{11}}
\newlabel{def:store_real@cref}{{[definition][13][]13}{11}}
\newlabel{lm:st_weak}{{14}{11}}
\newlabel{lm:st_weak@cref}{{[lemma][14][]14}{11}}
\newlabel{rmk:adequacy}{{16}{12}}
\newlabel{rmk:adequacy@cref}{{[remark][16][]16}{12}}
\newlabel{lm:adequacy}{{17}{12}}
\newlabel{lm:adequacy@cref}{{[theorem][17][1]17}{12}}
\citation{AriDowHerNakSau12}
\citation{Munch09}
\citation{Lepigre16}
\citation{Munch09}
\citation{Lepigre16}
\newlabel{thm:normalization}{{20}{14}}
\newlabel{thm:normalization@cref}{{[theorem][20][1]20}{14}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Extension to 2$^{\text  {nd}}$-order type systems}{14}}
\citation{AriDowHerNakSau12}
\citation{these}
\citation{these}
\citation{Herbelin12}
\citation{ChaFel12}
\citation{GarEtAl10}
\citation{Kesner16}
\citation{PedSau16}
\citation{AriDowHerNakSau12}
\citation{ChaFel12}
\citation{AriDowHerNakSau12}
\bibdata{biblio-en}
\bibcite{AriFel93}{1}
\@writefile{toc}{\contentsline {section}{\numberline {3}Conclusion and further work}{15}}
\newlabel{s:conclusion}{{3}{15}}
\newlabel{s:conclusion@cref}{{[section][3][]3}{15}}
\bibcite{AriDowHerNakSau12}{2}
\bibcite{BarBer96a}{3}
\bibcite{ChaFel12}{4}
\bibcite{Crolard99}{5}
\bibcite{CurHer00}{6}
\bibcite{DagSch15}{7}
\bibcite{FelFriKohDub86}{8}
\bibcite{Gallier90}{9}
\bibcite{GarEtAl10}{10}
\bibcite{Girard71}{11}
\bibcite{GuiMiq16}{12}
\bibcite{GuiM16}{13}
\bibcite{HerbelinHdR}{14}
\bibcite{Herbelin12}{15}
\bibcite{Kesner16}{16}
\bibcite{Krivine93}{17}
\bibcite{Krivine03}{18}
\bibcite{Krivine04}{19}
\bibcite{Krivine11}{20}
\bibcite{Krivine12}{21}
\bibcite{Krivine14}{22}
\bibcite{LafReuStr93}{23}
\bibcite{Lang07}{24}
\bibcite{Lepigre16}{25}
\bibcite{MarOdeWad98}{26}
\bibcite{Miquel11}{27}
\bibcite{these}{28}
\bibcite{Munch09}{29}
\bibcite{OkaLeeTar94}{30}
\bibcite{Parigot91}{31}
\bibcite{Parigot00}{32}
\bibcite{PedSau16}{33}
\bibcite{Plotkin75}{34}
\bibcite{Polonowski04}{35}
\bibcite{Tait67}{36}
\@writefile{toc}{\contentsline {section}{\numberline {A}Subject reduction of the {\relax {$\overline  {\lambda }_{[\lowercase {lv}\tau \star ]}$}}-calculus}{18}}
\newlabel{s:sub_red}{{A}{18}}
\newlabel{s:sub_red@cref}{{[subappendix][1][2147483647]A}{18}}
\newlabel{lm:lbvtstar_weak}{{21}{18}}
\newlabel{lm:lbvtstar_weak@cref}{{[lemma][21][2147483647]21}{18}}
\@writefile{toc}{\contentsline {section}{\numberline {B}Adequacy lemma}{21}}
\newlabel{a:real}{{B}{21}}
\newlabel{a:real@cref}{{[subappendix][2][2147483647]B}{21}}
