\documentclass[landscape]{slides}
\usepackage{fpslides}
\usepackage{color}
\usepackage{amssymb}
\usepackage{eepic/epic}
\usepackage{eepic/eepic}

\newcommand{\meta}[1]{{\color{green} #1}}

\newcommand{\obj}[1]{{\color{blue} #1}}
\newcommand{\dv}[1]{{\color{red} #1}}
\newcommand{\lftyp}[1]{{\color{blue} #1}}
\newcommand{\lfobj}[1]{{\color{red} #1}}

\newcommand{\ctr}[1]{\begin{array}[c]{c}#1\end{array}}
% \newenvironment{meta}{\begingroup \color{red}}{\endgroup}
% \newenvironment{obj}{\begingroup \color{blue}}{\endgroup}

\newcommand{\imp}{\supset}
\newcommand{\lfimp}{\mathrel{{\rm imp}}}
\newcommand{\rep}[1]{\ulcorner #1\urcorner}
\newcommand{\type}{{\rm type}}
\newcommand{\hil}[1]{{\rm hil}\, #1}
\newcommand{\Mtwo}{\mathcal{M}_2}
\newcommand{\Momega}{\mathcal{M}_\omega}
\newcommand{\foldn}{FO\lambda^{\Delta I\!\!N}}

\renewcommand{\theslide}{\arabic{slide}}

\input fpsfonts.def
%
% Normal Width (61)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Extra Width (70)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Small (73)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Small, Extra Width (85)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Height:
%   Normal: 17 or 18 lines?
%   Small: ??

\pagestyle{plain}
\sloppy
\raggedright
\renewcommand{\arraystretch}{1.5}

\begin{document}

 \begin{slide}{}
  \begin{center}
  {\bf Automated Theorem Proving in a Simple Meta-Logic for LF} \\[1em]
  Carsten Sch{\"u}rmann \\
  joint work with Frank Pfenning \\[1em]
  CADE-15, Lindau, Germany \\
  July 8, 1998
  \end{center}

  \vspace{1em}
  \begin{enumerate} \itemsep 0pt
   \item Reasoning About Deductions
   \item Leveraging the Logical Framework
   \item The Meta-Logic $\Mtwo$ for LF
   \item Experimental Results
   \item Conclusion
  \end{enumerate}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Deductive Systems}
 \begin{itemize} \itemsep 0pt
  \item Define a language
    \[ \obj{A} \bnfas \obj{P} \bnfalt \obj{A \imp A} \]
  \item Define a judgment via axioms and inference rules
    \[ \begin{array}{rcl}
     \dv{K_{\obj{A,B}}} & : & \obj{\vd A \imp (B \imp A)} \\
     \dv{S_{\obj{A,B,C}}} & : & \obj{\vd (A \imp (B \imp C)) \imp (A \imp B) \imp A \imp C} \\[1em]
     \dv{M\!P_{\obj{A,B}}} & : & \dv{\raisebox{-1.2ex}{\ibnc{\obj{\vd A \imp
B}}{\obj{\vd A}}{\obj{\vd B}}{}}}
    \end{array} \]
  \item Pervasive use of schematic judgments
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
 \slidetitle{Automated Deduction}
 \begin{itemize} \itemsep 0pt
  \item Traditional theorem proving: Searching For Deductions
   \begin{quote}
    \meta{Does there exist a deduction \dv{$H_{A}$} of \obj{$\vd A
\imp A$}?}
   \end{quote}
%   \item Some general techniques:
%   \begin{itemize} \itemsep 0pt
%    \item Unification for schematic variables
%    \item Resolution (forwards or backwards) using indexing, subsumption
%   \end{itemize}
   \item Our goal: Reasoning About Deductions
  \begin{itemize} \itemsep 0pt
   \item Soundness and completeness of proof procedures
   \begin{quote}
    \meta{For every \dv{$D$} of \obj{$\vd A$} there is an \dv{$E$}
of \obj{$\vd^{\!\!{}^-} A$}.}
   \end{quote}
   \item Consistency and cut-elimination
   \begin{quote}
    \meta{For every \dv{$D$} of \obj{$\Gamma \Longrightarrow A$}
and \dv{$E$} of \obj{$\Gamma, A \Longrightarrow C$} \\
  there exists an \dv{$F$} of \obj{$\Gamma \Longrightarrow C$}.}
   \end{quote}
   \end{itemize}
  \end{itemize}
  \vfill 
 \end{slide}

%
% \begin{slide}{}
%  \slidetitle{Reasoning About Deductions, Some Examples}
%  \begin{itemize} \itemsep 0pt
%   \item Soundness and completeness of proof procedures
%   \begin{quote}
%    \meta{For every \dv{$D$} of \obj{$\vd A$} there is an \dv{$E$}
%of \obj{$\vd^{\!\!{}^-} A$}.}
%   \end{quote}
%   \item Consistency and cut-elimination
%   \begin{quote}
%    \meta{For every \dv{$D$} of \obj{$\Gamma \Longrightarrow A$}
%and \dv{$E$} of \obj{$\Gamma, A \Longrightarrow C$} \\
%  there exists an \dv{$F$} of \obj{$\Gamma \Longrightarrow C$}.}
%   \end{quote}
%   \item Logical interpretations
%   \begin{quote}
%    \meta{For every \dv{$D$} of \obj{$\vd A$} there is an \dv{$E$} of
%\obj{$\vd^{\!\!{}^+} A^+$}.}
%   \end{quote}
%   \item Type preservation
%  \begin{quote}
%   \meta{For every \dv{$D$} of \obj{$e \evalsto v$} and \dv{$P$} of
%\obj{$e \hastype \tau$} there exists a \dv{$Q$} of \obj{$v \hastype \tau$}.}
%  \end{quote}
%   % \item Compiler correctness, $\ldots$
%  \end{itemize}
% \vfill
% \end{slide}

 
 \begin{slide}{}
  \slidetitle{Example: Hilbert's Deduction Theorem}
 \begin{itemize} \itemsep 0pt
 \item Requires hypothetical judgment \obj{$A \vd B$}
  \item {\bf Theorem:} \meta{For every \dv{$D$} of \obj{$A \vd B$} there
exists an \dv{$E$} of \obj{$\vd A \imp B$}.}
  \item {\bf Proof:} By induction on the structure of \dv{$D$}.
  \item {\bf Case:} $\dv{D} = \obj{A \vd A}$.  Then
  \begin{tabbing}
    % M\!P (M\!P (S_{A, A\imp A, A}, K_{A, A\imp A}), K_{A, A}) \quad \mbox{derives} \quad \obj{\vd A \imp A}
  \meta{\dv{$M\!P\; (M\!P\; S\; K)\; K$} of \obj{$\vd A \imp A$}} \` \quad
\meta{by rules}
  \end{tabbing}
  \item This case: pure resolution
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Proof Continued}
 \begin{itemize} \itemsep 0pt
  \item {\bf Case:} \dv{$D = \raisebox{-1.2ex}{\ibnc{\ctr{D_1 \\ \obj{A \vd B \imp
C}}}{\ctr{D_2 \\ \obj{A \vd B}}}{\obj{A \vd C}}{}}$}.
  \begin{tabbing}
   \meta{\dv{$E_1$} of \obj{$\vd A \imp (B \imp C)$}} \` \meta{by i.h.\
on \dv{$D_1$}} \\
   \meta{\dv{$E_2$} of \obj{$\vd A \imp B$}} \` \meta{by i.h.\ on \dv{$D_2$}} \\
   % \meta{$S_{A,B,C} (E_1, E_2)$ of $\vd A \imp C$} \` \meta{by rule}
   \meta{\dv{$M\!P\; (M\!P \;S\; E_1)\; E_2$} of \obj{$\vd A \imp C$}} \`
\meta{by rules}
  \end{tabbing}
  \item This case: induction hypotheses, resolution
  \item Two remaining cases: resolution
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
 \slidetitle{Reduction to Theorem Proving}
 \begin{itemize} \itemsep 0pt
  \item Encode judgments and derivations in a meta-logic
   \begin{quote}
    \meta{${\rm ded}(\rep{E}, \rep{A})$}
    iff \meta{\dv{$E$} is a derivation of \obj{$\vd A$}}.
    \meta{${\rm entails}(\rep{D}, \rep{A}, \rep{B})$}
    iff \meta{\dv{$D$} is a derivation of \obj{$A \vd B$}}.
   \end{quote}
  \item Encode and prove the Deduction Theorem 
  \begin{quote}
   \meta{$\forall A\ldot\forall B\ldot \forall D\ldot {\rm
entails}(D,A,B) \Rightarrow \exists E\ldot {\rm ded}(E, {\rm imp}(A,
B))$}
  \end{quote}
  \item Additional lemmas must be proven explicitly, 
    which could be assumed statically.

  \item Increased search space: \meta{${\rm ded}(\rep{E}, \rep{A})$} 
    must be proven explicitly, which could be checked statically.

%  \item Back to theorem proving
%  \begin{quote}
%    \meta{Is there a deduction \dv{Q} of \obj{$\vd^{\!\!^{M}} \forall
%A\ldot \forall B\ldot \forall D\ldot {\rm entails}(D,A,B) \Rightarrow
%\exists E\ldot {\rm ded}(E, {\rm imp}(A, B))$}?}
%  \end{quote}
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
 \slidetitle{Automating Meta-Theory}
 \begin{itemize} \itemsep 0pt
  \item Degree of automation depends critically on
  \begin{itemize} \itemsep 0pt
    \item directness of encoding \\
    \item reasoning principles in meta-logic
  \end{itemize}
  \item Quantifier-free inductive definitions \\ \relax
        [Shankar'87] Nqthm,
        [Matthews'94] FS$_0$, $\ldots$ \\
  \item Inductive type theories \\ \relax
        [Basin \& Constable'93] Nuprl,
        [McKinna \& Pollack'93] Lego,\\ \relax
        [Barras \& Werner'97] Coq, $\ldots$
 \end{itemize}
   
  \vfill 
 \end{slide}


 \begin{slide}{}
 \slidetitle{Claim}
 \begin{itemize} \itemsep 0pt
  \item Automating the meta-theory of deductive systems is
  \begin{itemize} \itemsep 0pt
   \item different enough and
   \item important enough
  \end{itemize}
  to warrant investigation of special-purpose theorem
proving techniques.
 \item Applications: language design, logic design, theorem proving
verification, secure mobile code, certifying compilation, etc.
\item Other special purpose theorem provers: geometry theorem proving,
  model checking, arithmetic, various constraint systems, etc.
 \end{itemize}
  \vfill 
 \end{slide}


 \begin{slide}{}
  \slidetitle{Logical Frameworks}
 \begin{itemize} \itemsep 0pt
  \item Specialized meta-languages for direct representation of
deductive systems
  \item LF [Elf, Twelf]
  \begin{itemize} \itemsep 0pt
   \item dependently typed $\lambda$-calculus
   \item schematic judgments
   \item hypothetical judgments
  \end{itemize}
  \begin{itemize} \itemsep 0pt
   \item judgments as types \\
 \( \lftyp{A} \bnfas \lftyp{a\, M_1\ldots M_n} \bnfalt \lftyp{\Pi x\oftp
A_1\ldot A_2} \bnfalt \lftyp{A_1 \arrow A_2} \)
   \item deductions as objects \\
 \( \lfobj{M} \bnfas \lfobj{c} \bnfalt \lfobj{x} \bnfalt \lfobj{\lam x\oftp A\ldot M} \bnfalt \lfobj{M_1\, M_2}\)
  \end{itemize}
  \item Hereditary Harrop formulas (FOHH) [Isabelle, $\lambda$Prolog]
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Hilbert Calculus in LF}
 \begin{itemize} \itemsep 0pt
    \item Propositions: \meta{$\lftyp{\rep{A}} : \lftyp{o}$}
     
 \meta{
 \( \renewcommand{\arraystretch}{1}
  \begin{array}{lcl}
  \lftyp{o} & : & \lftyp{\type} \\[1ex]
  \lftyp{\lfimp} & : & \lftyp{o \arrow o \arrow o} \hspace{8cm}
  \mbox{\color{black} \textit{using infix \lftyp{$\lfimp$}}}
 \end{array} \)
  }
  \bigskip

  \item Deductions: $\meta{\lfobj{\rep{D}} \hastype \lftyp{\hil{\rep{A}}}}$ iff
\meta{\dv{$D$} deduction of \obj{$\vd A$}}

 \meta{
 \( \renewcommand{\arraystretch}{1}
  \begin{array}{lcl}
  \lftyp{\hil{}} & : & \lftyp{o \arrow \type} \\[1ex]
  \lfobj{K} & : & \lftyp{\hil{(A \lfimp (B \lfimp A))}} \\
  \lfobj{S} & : & \lftyp{\hil{((A \lfimp (B \lfimp C)) \lfimp (A \lfimp B) \lfimp A \lfimp C)}} \\
  \lfobj{M\!P} & : & \lftyp{\hil{(A \lfimp B)} \arrow \hil{A} \arrow \hil{B}}
 \end{array} \)
  }
  \end{itemize}
 
  \vfill
 \end{slide}


 \begin{slide}{}
 \slidetitle{Reasoning About Deductions in LF}
 \begin{itemize} \itemsep 0pt
  \item Hypothetical judgments: 
 \begin{quote}
 \meta{$\lfobj{\rep{E}} \hastype \lftyp{\hil{\rep{A}} \arrow
\hil{\rep{B}}}$} iff \meta{\dv{$E$} deduction of \obj{$A \vd B$}}
 \end{quote}
  \item Cannot prove properties of such functions \emph{within} LF
  \item Add one more layer to reason \emph{about} LF objects
  \item Meta-logic design criteria
    \begin{itemize} \itemsep 0pt
    \item Meta-theoretic proofs should be expressible
    \item Embedding of the logical framework should be direct
    \end{itemize}
 \end{itemize}
  \vfill 
 \end{slide}


 \begin{slide}{}
  \slidetitle{$\Mtwo$, a Simple Meta-Logic for LF}
  \begin{itemize} \itemsep 0pt
   \item Formulas quantify over \emph{closed} LF objects.
   \[ \meta{F} \bnfas \meta{\forall \lfobj{x_1}\oftp \lftyp{A_1}\ldots
\forall \lfobj{x_n}\oftp \lftyp{A_n} \ldot \exists \lfobj{y_1}\oftp
\lftyp{B_1}\ldots \exists \lfobj{y_m}\oftp \lftyp{B_m}\ldot \top} \]
   \item Judgment
   \[ \meta{\lfobj{\Gamma}; \Delta \vd_{\!\!{}_{\lfobj{\Sigma}}} P \in F} \]
   where \lfobj{$\Sigma$} is an LF signature, \\
   \lfobj{$\Gamma$} is an LF context, \\
   \meta{$\Delta$} contains lemmas and ``inductive assumptions'', \\
   \meta{$P$} is a (meta-)proof term, \\
   \meta{$F$} is meta-logic formula
   \item No primitive predicates
   \item Expressive power stems from LF
  \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Some Sequent Rules for $\Mtwo$}
 \begin{itemize} \itemsep 0pt
  \item Filling \lfobj{$x$}:
  \meta{
  \[ \ibnc{\lfobj{\Gamma} \vd^{\!\!{}^{LF}}_{\!\!{}_{\lfobj{\Sigma}}}
\lfobj{M} \hastype \lftyp{A}}{\lfobj{\Gamma}; \Delta \vd P \in
[\lfobj{M}/\lfobj{x}]F}{\lfobj{\Gamma}; \Delta \vd \langle \lfobj{M},
P\rangle \in \exists \lfobj{x}\oftp \lftyp{A}\ldot F}{\exists{\rm R}} \]
  }
  \item Recursion:
  \meta{
 \[ \ianc{\lfobj{\Gamma}; (\Delta, {\mathbf x}\in F)
\vd_{\!\!{}_{\lfobj{\Sigma}}} P \in F}{\lfobj{\Gamma}; \Delta
\vd_{\!\!{}_{\lfobj{\Sigma}}} (\mu {\mathbf x}\in F\ldot P) \in F}{{\rm
fix}} \]
  }
   where \meta{$\mu {\mathbf x} \in F\ldot P$} terminates in
\meta{${\mathbf x}$}.
  \item Splitting $\lfobj{x}$:
   \meta{
   \[ \ibnc{\lfobj{\Gamma(x)} = \lftyp{B}}{\lfobj{\Gamma}; \Delta
\vd_{\!\!{}_{\lfobj{\Sigma}}} \Omega \;{\rm covers}\; \lftyp{B}\;{\rm in}\;
F}{\lfobj{\Gamma}; \Delta \vd_{\!\!{}_{\lfobj{\Sigma}}} {\rm case}\; x\;
{\rm of}\; \Omega \in F}{{\rm case}} \]
  }
  where \meta{$\Omega$} is a pattern matching expression.
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
 \slidetitle{Correctness}
 \begin{itemize} \itemsep 0pt
  \item {\bf Theorem:}
 \begin{quote}
 If \meta{$\lfobj{\cdot}; \cdot \vd_{\!\!{}_{\lfobj{\Sigma}}} P \in \forall
\lfobj{x_1}\oftp \lftyp{A_1}\ldots \forall \lfobj{x_n}\oftp \lftyp{A_n}
\ldot \exists \lfobj{y_1}\oftp \lftyp{B_1}\ldots \exists \lfobj{y_m}\oftp
\lftyp{B_m}\ldot \top$} then \\
 for all \emph{closed} LF objects \meta{$\lfobj{M_1}\oftp \lftyp{A_1},
\ldots, \lfobj{M_n}\oftp \lftyp{A_n}$} \\
 there exist \emph{closed} LF objects \meta{$\lfobj{N_1} \oftp
\lftyp{B_1}, \ldots, \lfobj{N_m} \oftp \lftyp{B_m}$} \\
 over signature $\lfobj{\Sigma}$.
 \end{quote}
  \item {\bf Proof sketch:} Define an operational semantics for proof
term \meta{$P$} in $\Mtwo$ and show
  \begin{enumerate} \itemsep 0pt
   \item type preservation,
   \item progress, and
   \item termination.
  \end{enumerate}
 \end{itemize}
  \vfill 
 \end{slide}


 \begin{slide}{}
  \slidetitle{Example: Hilbert's Deduction Theorem}
 \begin{itemize} \itemsep 0pt
  \item {\bf Theorem:}
  \[ \meta{\forall \lftyp{A}\oftp \lftyp{o}\ldot \forall \lftyp{B}\oftp
 \lftyp{o}\ldot \forall \lfobj{D}\oftp \lftyp{(\hil{A} \arrow \hil{B})}
\ldot \exists \lfobj{E}\oftp \lftyp{\hil (A\, \lfimp B)}\ldot \top} \]
  \item Proof term: A total function mapping \\
    \begin{center}
    objects of type $\lftyp{(\hil{A} \arrow \hil{B})}$ \\
    to\\
    objects of type $\lftyp{\hil{(A \lfimp B)}}$\\
  \end{center}
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Example: Hilbert's Deduction Theorem}
 \begin{itemize} \itemsep 0pt
  \item {\bf Theorem:}
  \[ \meta{\forall \lftyp{A}\oftp \lftyp{o}\ldot \forall \lftyp{B}\oftp
 \lftyp{o}\ldot \forall \lfobj{D}\oftp \lftyp{(\hil{A} \arrow \hil{B})}
\ldot \exists \lfobj{E}\oftp \lftyp{\hil (A\, \lfimp B)}\ldot \top} \]
  \item Proof term:
  \meta{
  \[ \renewcommand{\arraystretch}{1}
  \begin{array}{r@{\;}lcl}
   \multicolumn{3}{l}{{\rm abs}_{A,B} : \lftyp{(\hil{A} \arrow \hil{B})}
\Rightarrow \lftyp{\hil{(A \lfimp B)}}} \\[1ex]
   {\bf fun} & {\rm abs}\; \lfobj{(\lam x\ldot x)} & = & \lfobj{M\!P\;
(M\!P\; S\; K)\; K} \\
        \mid & {\rm abs}\; \lfobj{(\lam x\ldot K)} & = & \lfobj{M\!P\;
K\; K} \\
        \mid & {\rm abs}\; \lfobj{(\lam x\ldot S)} & = & \lfobj{M\!P\;
K\; S} \\
        \mid & {\rm abs}\; \lfobj{(\lam x\ldot M\!P\; (D_1\; x)\;
(D_2\; x))} & = \\
 & \hspace{1em} {\bf let} \\
 & \hspace{3em} {\bf val}\; \lfobj{E_1} = {\rm abs}\; \lfobj{(\lam x\ldot D_1\; x)} \\
 & \hspace{3em} {\bf val}\; \lfobj{E_2} = {\rm abs}\; \lfobj{(\lam x\ldot D_2\; x)} \\
 & \hspace{1em} {\bf in} \\
 & \hspace{3em} \lfobj{M\!P\; (M\!P\; S\; E_1)\; E_2} \\
 & \hspace{1em} {\bf end}
  \end{array} \]
  }
 \end{itemize}
  \vfill
 \end{slide}



 \begin{slide}{}
  \slidetitle{Strategy}
  \begin{itemize} \itemsep 0pt
   \item Input: signature, theorem, bound, termination ordering
  \end{itemize}
   \begin{center}
    \input{strat.eepic}
   \end{center}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Strategy Remarks}
 \begin{itemize} \itemsep 0pt
  \item Bounds ensure termination, no backtracking
  \begin{itemize} \itemsep 0pt
   \item {\bf Filling:} Size bound on terms
   \item {\bf Recursion:} Number of recursive calls
   \item {\bf Splitting:} Splitting depth
  \end{itemize}
  \item Termination orders are lexicographic/simultaneous extensions
    of subterm orderings
  \item Dependent types restrict search space for Filling and Splitting
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{The Twelf Implementation}
 \begin{itemize} \itemsep 0pt
  \item In Standard ML
  \item Dependently typed explicit substitutions
%  \item ``Compilation'' of signatures
  \item Pattern unification and constraint simplification
  \item Extract realizing functions as relations
  \item Very few optimizations (unification by effect)
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Experimental Results, FRS}
 \renewcommand{\arraystretch}{1}
\begin{center}
\begin{tabular}{|l|r|r|r|r|r|}
  \hline         
  {\bf Experiment}&{\bf Fill}&{\bf Split}&{\bf Rec}&{\bf Total}\\
  \hline
  Cartesian Closed Categories&1.000&0.004&0.036&1.099\\
  \hline
  CPM Completeness&0.916&0.010&0.117&1.134\\
  CPM Proof equivalence: $\Rightarrow$ &0.226&0.034&0.442&0.951\\
  CPM Proof equivalence: $\Leftarrow$ &0.280&0.033&0.647&1.235\\
  \hline
  Horn LP Soundness&4.336&0.004&0.049&4.501\\
  Horn LP Canonical forms&0.028&0.009&0.107&0.303\\
  Horn LP Completeness&0.015&0.005&0.039&0.195\\
  \hline
  Mini-ML Value soundness &0.016&0.041&0.061&0.172\\
  Mini-ML Type preservation&0.062&0.521&0.150&0.799\\
  Mini-ML Evaluation/Reduction&25.397&0.007&0.078&25.546\\
  \hline
  Hilbert's deduction theorem&0.197&0.004&0.010&0.322\\
  \hline
  Associativity of $+$&0.009&0.012&0.016&0.063\\
  Commutativity of $+$&0.092&0.609&4.139&4.877  \\
\hline
\end{tabular}
\end{center}
\medskip
Linux 2.30, SML/NJ 110, Twelf 1.2 on Pentium II (300 Mhz)
  \vfill
 \end{slide}



 \begin{slide}{}
  \slidetitle{Related Work}
 \begin{itemize} \itemsep 0pt
  \item $\foldn$ over FOHH [McDowell \& Miller'97]
  \begin{itemize} \itemsep 0pt
   \item definitional reflection ($\sim$ splitting)
   \item only natural number induction
   \item interactive
  \end{itemize}
  \item HALF [G\"oteborg]
  \begin{itemize} \itemsep 0pt
   \item one-level architecture, proof editor
   \item filling, splitting, recursion
  \end{itemize}
  \item Schema checking [Rohwedder]
  \begin{itemize} \itemsep 0pt
   \item decidable meta-theory: little automation
   \item larger class of proofs
  \end{itemize}
 \end{itemize}
  \vfill
 \end{slide}


 \begin{slide}{}
  \slidetitle{Future Work}
 \begin{itemize} \itemsep 0pt
  \item Automatic appeal to lemmas
  \item Complete induction
  \item Complex termination orderings
  \item Richer meta-logic ($\Momega$, beyond)
  \item Reasoning about open LF objects in regular contexts
 \end{itemize}
  \vfill
 \end{slide}

%
% \begin{slide}{}
%  \slidetitle{Future Work}
% \begin{itemize} \itemsep 0pt
%  \item Case studies:
%  \begin{itemize} \itemsep 0pt
%   \item cut elimination
%   \item natural deduction and sequent calculi
%   \item compiler correctness
%  \end{itemize}
%  \item Linear Logical Framework [Cervesato \& Pf'97]
%  \begin{itemize} \itemsep 0pt
%   \item protocols
%   \item properties of imperative languages, abstract machines
%   \item proof-carrying code
%   \item verification of safety policy
%  \end{itemize}
% \end{itemize}
%  \vfill
% \end{slide}


 \begin{slide}{}
  \slidetitle{Summary}
 \begin{itemize} \itemsep 0pt
  \item $\Mtwo$ a simple meta-logic over LF
  \item Can prove a number of meta-theorems automatically \\
        soundness and completeness of Horn-LP, correctness of
        abstract machines, type preservation for Mini-ML,
        deduction theorem
  \item Simple-minded strategy
  \item Effectiveness due to expressive power of LF
  \item Ongoing work:
  \begin{itemize} \itemsep 0pt
   \item Lemmas
   \item Generalization to regular hypothetical judgments
   \item Efficiency and strategy improvements
   \item Linear logical framework
  \end{itemize}
 \end{itemize}
  \vfill
 \end{slide}

%
% \begin{slide}{}
%  \slidetitle{Problems with an inductive definition of LF}
%  \begin{itemize} \itemsep 0pt
%   \item variables as deBruijn indices: reimplement unification, substitution
%   \item inference rules as constructors: reimplement resolution,
%         hypothetical reasoning
%   \item must prove \emph{many} deep properties of LF
% \end{itemize}
%  \vfill
% \end{slide}
%
% \begin{slide}{}
%  \slidetitle{Experimental Results, RFS}
% \renewcommand{\arraystretch}{1}
%\begin{center}
%\begin{tabular}{|l|r|r|r|r|r|}
%  \hline
%  {\bf Experiment}&{\bf Fill}&{\bf Split}&{\bf Rec}&{\bf Total}\\
%  \hline
%  Cartesian Closed Categories&0.312&0.004&0.058&0.437\\
%  \hline
%  CPM Completeness&0.209&0.024&0.310&0.611\\
%  CPM Proof equivalence: $\Rightarrow$ &0.058&0.063&0.609&0.953\\
%  CPM Proof equivalence: $\Leftarrow$ &0.083&0.063&0.551&0.924\\
%  \hline
%  Horn LP Soundness&1.004&0.004&0.081&1.194\\
%  Horn LP Canonical forms&0.015&0.010&0.194&0.337\\
%  Horn LP Completeness&0.008&0.005&0.072&0.262\\
%  \hline
%  Mini-ML Value soundness &0.008&0.027&0.113&0.188\\
%  Mini-ML Type preservation&0.033&0.523&0.233&0.837\\
%  Mini-ML Evaluation/Reduction &1.778&0.007&0.102&1.952\\
%  \hline
%  Hilbert's abstraction theorem&0.080&0.004&0.023&0.166\\
%  \hline
%  Associativity of $+$&-&-&-&-\\
%  Commutativity of $+$&0.078&0.604&12.608&13.327   \\
%  \hline
%\end{tabular}
%\end{center}
%\medskip
%Linux 2.30, SML/NJ 110, Twelf 1.2 on Pentium II (300 Mhz)
%  \vfill
% \end{slide}

\end{document}
