\documentclass{article}
\usepackage{euler,proof,amstext,longtable,fullpage,amssymb}
\begin{document}

\newcommand{\N}[1]{\text{\rm\ttfamily\mdseries{#1}}}
\newcommand{\Head}[1]{\newpage\multicolumn{2}{l}
  {\addtocounter{section}{1}
    \addcontentsline{toc}{section}{\protect\numberline{\thesection} #1}
    \setcounter{subsection}{0}\Large\bfseries\thesection\quad{#1}}}
\newcommand{\Subhead}[1]{\multicolumn{2}{l}
  {\addtocounter{subsection}{1} 
    \addcontentsline{toc}{subsection}{\protect\numberline{\thesubsection} #1}
    \large\bfseries\thesubsection\quad #1}}

\newcommand{\Infer}[2]{\infer{#2}{#1}}
\newcommand{\Step}[3]{\mbox{\infer[\text{#1}]{#2}{#3}}}
\newcommand{\Use}[2]{\mbox{\infer*{#1}{#2}}}
\newcommand{\invert}{\ensuremath{\downarrow}}

\newcommand{\Class}[2]{\fbox{\N{#2} ::= $\cdots$} & \fbox{#1}}
\newcommand{\Def}[3]{\fbox{\N{#2} $\equiv$ {#3}} & \fbox{#1}}
\newcommand{\Syntax}[3]{#3 ::= #2 & \text{(#1)}}
\newcommand{\Scheme}[2]{\fbox{#2} & \fbox{#1}}
\newcommand{\Axiom}[2]{{#2} & \text{(#1)}}
\newcommand{\Rule}[3]{\infer{#3}{#2} & \raisebox{1.5ex}{\text{(#1)}}}
\newcommand{\Thm}[3]{\fbox{\Infer{#2}{#3}} & \fbox{#1}}
\newcommand{\Prooft}[2]{{#2} & \text{(#1)}\index{#1}}
\newcommand{\Proofp}[1]{& \text{(#1)}\index{#1}} 
\newcommand{\Point}[1]{\multicolumn{1}{l}#1}


\newcommand{\zx}[0]{@x@}
\newcommand{\zy}[0]{@y@}
\newcommand{\zc}[0]{@c@}
\newcommand{\zd}[0]{@d@}
\newcommand{\zp}[0]{@p@}
\newcommand{\zptop}[0]{@top@}
\newcommand{\zpc}[1]{@#1@}
\newcommand{\zpvar}[1]{@#1@}
\newcommand{\zpcat}[2]{@#1,#2@}
\newcommand{\zj}[0]{@j@}
\newcommand{\zjz}[0]{@somepriv@}

\newcommand{\zl}[0]{@l@}
\newcommand{\zltop}[0]{@top@}
\newcommand{\zlcat}[2]{@#1,#2@}
\newcommand{\zlp}[2]{@#1:\ #2@}
\newcommand{\zlread}[2]{@#1:\ #2@}
\newcommand{\zltrust}[1]{@T\ #1@}

\newcommand{\zt}[0]{@t@}
\newcommand{\zu}[0]{@u@}
\newcommand{\ztu}[2]{@{#1}_{#2}@}
\newcommand{\zuunit}[0]{@unit@}
\newcommand{\ztbool}[1]{@bool_{#1}@}
%\newcommand{\ztfun}[3]{@[#1]#2 -> #3@}
\newcommand{\ztfun}[2]{@#1 -> #2@}
\newcommand{\zubool}[1]{@bool_{#1}@}
%\newcommand{\zufun}[3]{@[#1]#2 -> #3@}
\newcommand{\zufun}[2]{@#1 -> #2@}
\newcommand{\ztpsin}[1]{@{'#1}@}
\newcommand{\ztjsin}[1]{@{'#1}@}

\newcommand{\zut}[2]{@[[#1]]=#2@}
\newcommand{\zhg}[2]{@[[#1]]=#2@}

\newcommand{\zlab}[2]{@lab(#1)=#2@}
\newcommand{\zrelab}[3]{@relab(#1,#2)=#3@}
\newcommand{\zulab}[2]{@lab(#1)=#2@}
\newcommand{\zurelab}[3]{@relab(#1,#2)=#3@}

\newcommand{\za}[0]{@a@}
\newcommand{\zaz}[0]{@empty@}
\newcommand{\zal}[3]{@#1,#2\leq #3@}
\newcommand{\zap}[3]{@#1,#2\leq #3@}
\newcommand{\zr}[0]{@r@}
\newcommand{\zrz}[0]{@empty@}
\newcommand{\zrl}[3]{@#1,#2<:#3@}

\newcommand{\ze}[0]{@e@}
\newcommand{\zunit}[0]{@unit@}
\newcommand{\ztrue}[1]{@true_{#1}@}
\newcommand{\zfalse}[1]{@false_{#1}@}
\newcommand{\zvar}[1]{@#1@}
\newcommand{\zfun}[4]{@fun[#1]#2:#3. #4@}
\newcommand{\zapp}[2]{@#1\ #2@}
\newcommand{\zinst}[3]{@#1\ [#2/#3]@}
\newcommand{\zifb}[3]{@if\ #1\ #2\ #3@}
\newcommand{\zifl}[4]{@if (#1 <: #2)\ #3\ #4@}
\newcommand{\zifp}[4]{@if (#1 \leq  #2)\ #3\ #4@}
\newcommand{\ztag}[3]{@[#1\sqsubseteq #2]#3@}

\newcommand{\ztfresh}[1]{@fresh\ #1@}
\newcommand{\zfresh}[1]{@fresh\ #1@}
\newcommand{\zm}[0]{@m@}
\newcommand{\zmtrue}[1]{@true_{#1}@}
\newcommand{\zmfalse}[1]{@false_{#1}@}
\newcommand{\zmvar}[1]{@#1@}
%\newcommand{\zmfun}[4]{@fun[#1]#2:#3. #4@}
\newcommand{\zmfun}[3]{@fun #1:#2. #3@}
\newcommand{\zmapp}[2]{@#1\ #2@}
\newcommand{\zmifb}[3]{@if\ #1\ #2\ #3@}
\newcommand{\zmifl}[4]{@if (#1 <: #2)\ #3\ #4@}
\newcommand{\zmifp}[4]{@if (#1 \leq  #2)\ #3\ #4@}



\newcommand{\zg}[0]{@g@}
\newcommand{\zgz}[0]{@empty@}
\newcommand{\zgx}[3]{@#1,#2:#3@}
\newcommand{\zh}[0]{@h@}
\newcommand{\zhz}[0]{@empty@}
\newcommand{\zhx}[3]{@#1,#2:#3@}

\newcommand{\zperm}[2]{@#1 \equiv #2@}
\newcommand{\zxneq}[2]{@#1 \neq #2@}
\newcommand{\zneq}[2]{@#1 \neq #2@}
\newcommand{\zyneq}[2]{@#1 \neq #2@}
\newcommand{\zpsome}[1]{@some\ #1@}
\newcommand{\zjsome}[1]{@some\ #1@}
\newcommand{\zlsome}[1]{@some\ #1@}
\newcommand{\zusome}[1]{@some\ #1@}
\newcommand{\zasome}[1]{@some\ #1@}
\newcommand{\ztsome}[1]{@some\ #1@}
\newcommand{\zpst}[3]{@#1 |- #2 \leq #3@}
\newcommand{\zpnst}[3]{@#1 \not|- #2\leq  #3@}
\newcommand{\zlsty}[3]{@#1 |- #2 \diamond #3@}
\newcommand{\zpsty}[3]{@#1 |- #2 \diamond #3@}
\newcommand{\zjst}[2]{@#1 <: #2@}
\newcommand{\zust}[3]{@#1 |- #2 <: #3@}
\newcommand{\ztst}[3]{@#1 |- #2 <: #3@}
\newcommand{\zlst}[3]{@#1 |- #2 \sqsubseteq #3@}
\newcommand{\zlnst}[3]{@#1 |- #2 \not<: #3@}
\newcommand{\zast}[2]{@#1 \leq #2@}
\newcommand{\zanst}[2]{@#1 \not\leq #2@}
\newcommand{\zrst}[3]{@#1 |- #2 <: #3@}
\newcommand{\zljoin}[4]{@#1 |- #2 join #3 = #4@}
\newcommand{\zllm}[5]{@#1;#2 |- #3 meet #4 = #5@}
\newcommand{\ztjoin}[4]{@#1 |- #2 join #3 = #4@}
\newcommand{\ztlm}[5]{@#1;#2 |- #3 meet #4 = #5@}
\newcommand{\zalbar}[3]{@#1|#2=#3@}
\newcommand{\zarbar}[3]{@#1|#2=#3@}
\newcommand{\zaa}[2]{@#1|-#2@}
\newcommand{\zara}[3]{@#1;#2|-#3@}
\newcommand{\zarj}[4]{@#1;#2|-_1 #3 <# #4@}
\newcommand{\zlty}[2]{@#1 |-#2@}
\newcommand{\zty}[4]{@#1;#2 |- #3 : #4@}
\newcommand{\zmty}[4]{@#1;#2 |- #3 : #4@}
\newcommand{\zgxt}[3]{@#1[#2]=#3@}
\newcommand{\zhxt}[3]{@#1[#2]=#3@}

\newcommand{\zsub}[4]{@#1 \{#2 / #3\} = #4@}
\newcommand{\zeesub}[4]{@#1 \{#2 / #3\} = #4@}
\newcommand{\zepsub}[4]{@#1 \{#2/#3\} = #4@}
\newcommand{\zppsub}[4]{@#1 \{#2/#3\} = #4@}
\newcommand{\zapsub}[4]{@#1 \{#2/#3\} = #4@}
\newcommand{\zrpsub}[4]{@#1 \{#2/#3\} = #4@}
\newcommand{\ztpsub}[4]{@#1 \{#2/#3\} = #4@}
\newcommand{\zval}[1]{@val\ #1@}
\newcommand{\zar}[2]{@#1 |- #2@}
\newcommand{\znar}[2]{@#1 \not|- #2@}
\newcommand{\zpp}[3]{@#1|- #2 <: #3@}
\newcommand{\zpj}[3]{@#1|- #2 <# #3@}
\newcommand{\znpp}[3]{@#1 \not|- #2 <: #3@}
\newcommand{\znpj}[3]{@#1 \not|- #2 <# #3@}
\newcommand{\zao}[0]{@a^\bullet@}
\newcommand{\zaoz}[0]{@empty@}
\newcommand{\zaoa}[1]{@#1@}
\newcommand{\zas}[0]{@\bar{a}@}
\newcommand{\zasz}[0]{@empty@}
\newcommand{\zasa}[2]{@#1,#2@}
\newcommand{\zae}[2]{@#1 |- #2@}
\newcommand{\zaex}[2]{@#1 \Vdash #2@}
\newcommand{\zev}[3]{@#1 |- #2 --> #3@}
% \newcommand{\ztopev}[6]{@(#1;#2)|#3 --> (#4;#5)|#6@}
\newcommand{\ztopev}[5]{@(#1;#2)|#3 --> (#4;#5)@}
\newcommand{\zbigev}[4]{@(#1;#2) ==> (#3;#4)@}

\newcommand{\zq}[0]{@q@}
\newcommand{\zqz}[0]{@empty@}
\newcommand{\zqappa}[1]{@q\ #1@}
\newcommand{\zqappb}[1]{@#1\ q@}
\newcommand{\zqinst}[2]{@q\ [#1/#2]@}
\newcommand{\zqifb}[2]{@if\ q\ #1\ #2@}
\newcommand{\zqifpa}[3]{@if\ (q\leq #1)\ #2\ #3@}
\newcommand{\zqifpb}[3]{@if\ (#1\leq q)\ #2\ #3@}
\newcommand{\zqtag}[2]{@[#1\sqsubseteq #2]q@}
\newcommand{\zsplit}[3]{@#1 = #2[#3]@}
\newcommand{\zcombine}[3]{@#1[#2] = #3@}
\newcommand{\zreq}[2]{@req\ #1 = #2@}
\newcommand{\zve}[2]{@#1 |- ve\ #2@}
\newcommand{\ztopve}[2]{@#1 |- topve\ #2@}
\newcommand{\zsignal}[1]{@signal\ #1@}

\newcommand{\zz}[0]{@z@}
% \newcommand{\zh}[0]{@h@}
% \newcommand{\zhz}[0]{@\cdot@}
% \newcommand{\zhx}[3]{@(#1,#2|->#3)@}
% \newcommand{\zhdom}[2]{@dom(#1)=#2@}
\newcommand{\zmod}[2]{@#1 |= #2@}
\newcommand{\zxs}[0]{@\bar{x}@}
\newcommand{\znmem}[2]{@#1 \not\in #2@}
\newcommand{\zsubh}[3]{@#1(#2)=#3@}
\newcommand{\zqv}[5]{@#1 |- #2 ~_{#3} #4 : #5@}
\newcommand{\zqvx}[8]{@all (#1 |- #4 ~_{#6} #5 : #7). \
  #1 |-  (#2\ #4)  ~_{#6} (#3\ #5) : #8@}
\newcommand{\zassume}[6]{@assume\ #1 |- #2 ~~_{#3} #4 : #5@}
\newcommand{\zqe}[5]{@#1 |- #2 ~~_{#3} #4 : #5@}
\newcommand{\zqh}[5]{@#1 |- #2 ~_{#3} #4 : #5@}

\title{Dynamic Updating of Information-Flow Policies}
\author{
Michael Hicks\footnotemark[1]
\qquad Boniface Hicks\footnotemark[2]
\qquad Stephen Tse\footnotemark[3]
\qquad Steve Zdancewic\footnotemark[3] \\
\footnotemark[1]\ \ University of Maryland
\quad\footnotemark[2]\ \ Pennsylvania State University
\quad\footnotemark[3]\ \ University of Pennsylvania
}
\maketitle


This report is automatically generated by the tool \verb|lf2tex| from
the semantics specification \verb|update.elf| (Twelf source) and the
syntactic specification \verb|update.tex| (\LaTeX\ source).

  \bigskip
  Some notes about the typesetting used in this report:

  \begin{itemize}
  \item A syntax class is displayed boxed like \fbox{@e@ ::= $\cdots$}
    ({\em terms}).
  \item A syntax entity is displayed unboxed like @e@ ::= @fun x:t. e@
    ({\em functions}).
  \item A judgement form is displayed boxed like \fbox{@a;g |- e : t@}
    ({\em typings}).
  \item A judgement rule is displayed unboxed like 
    \Infer{@a;g,x:t1 |- e : t2@}{@a;g |- fun x:t.e : t1 -> t2@}
    ({\em typing for functions}).
  \item A theorem is displayed boxed like
    \fbox{\Infer{@a1;g |- e1:t@ & @(a1;e1) --> (a2;e2)@}
{@a2;g |- e2 : t@}} ({\em preservations}).

  \item A proof is displayed as a numbered list with the last one of
  the list being the conclusion. (A rule name with downarrow
  ($\downarrow\text{ty-fun}$) means by the inversion of such rule.)
  \end{itemize}


%\clearpage
\tableofcontents
\footnotesize
\begin{longtable}{cr}
\csname \@\@input\endcsname update.tex3
\end{longtable}
\end{document}