\documentclass{llncs}
\usepackage{latexsym}
\usepackage{cdsty}
\usepackage{amssymb}
\usepackage{fancyheadings}
\usepackage{functions}
%\usepackage{color}
\usepackage{epic}
\usepackage{eepic}
\input{def.tex}

\sloppy
%\textheight7.7in
%\textwidth5in

\newcommand{\Momega}{\mathcal{M}_\omega}
\newcommand{\Mtwo}{\mathcal{M}_2}
\newcommand{\foldn}{FO\lambda^{\Delta I\!\!N}}

\begin{document}
\bibliographystyle{alpha}
\pagestyle{plain}

\title{Automated Theorem Proving in a \\ Simple Meta Logic for LF\thanks{Draft from 3/26/98: latest version: {\tt http://www.cs.cmu.edu/$\sim$carsten/ps/m2.tar.gz}}}
\author{Carsten Sch\"urmann \and Frank Pfenning
  \thanks{This work was sponsored by NSF Grant CCR-9619584}}
\institute{Carnegie Mellon University\\
  School of Computer Science\\
  {\tt carsten@cs.cmu.edu \hspace{2em} fp@cs.cmu.edu}}
\date{\today}
\maketitle

%  Higher-order abstract syntax is a central representation technique
%  when representing deductive systems in logical frameworks: variables
%  of the object language are represented by variables of the meta
%  language.  On the one hand, encodings using this idea are often
%  extremely concise and elegant, on the other, higher-order
%  representations are no longer inductive, which means that standard
%  techniques for reasoning by induction do not apply.
  
%  In this paper, we present a meta-logic for LF which overcomes this
%  problem by realizing inductive proofs as total functions.  It uses
%  recursion and pattern-matching to mimic strong induction principles.
%  Because of the elegant representation of deductions using dependent
%  types it is possible to devise an efficient proof search algorithm
%  for this meta logic.  It has been implemented as an automated
%  theorem prover for the proof assistant Twelf, a reimplementation and
%  extension of the logic programming language Elf.  Twelf has been
%  used to prove fully automatically (among others) the type
%  preservation result for Mini-ML \cite{Pfenning94un}.
\begin{abstract}
Higher-order representation techniques allow elegant encodings of logics
and programming languages in the logical framework LF, but unfortunately
they are fundamentally incompatible with induction principles needed to
reason about them.  In this paper we develop a meta-logic $\Mtwo$ which
allows inductive reasoning over such LF encodings, and describe its
implementation in Twelf, a special-purpose automated theorem prover for
properties of logics and programming languages.  We have used Twelf to
automatically prove a number of non-trivial theorems, including type
preservation for Mini-ML and the deduction theorem for intuitionistic
propositional logic.
\end{abstract}

%-----------------------------------------------------------------------

\section{Introduction} \label{sec:intro}

The logical framework LF~\cite{Harper93jacm} has been designed as a
meta-language for representing deductive systems which are common in the
study of logics and programming languages.  It allows concise encodings
of many common inference systems, such as natural deduction and sequent
calculi, type systems, operational semantics, compilers, abstract
machines, etc. (see~\cite{Pfenning96caap} for a survey).  These
representations often lead directly to implementations, either via the
constraint logic programming paradigm~\cite{Pfenning94cade} or via
general search using tactics and tacticals.

The logical framework derives its expressive power from the use of
dependent types together with ``higher-order'' representation techniques
which directly support common concepts in deductive systems, such as
variable binding and capture-avoiding substitution, parametric and
hypothetical judgments, and substitution properties.  The fact that
these notions are an integral part of the logical framework would seem
to make it an ideal candidate not only for reasoning \emph{within}
various inference systems, but for reasoning \emph{about} properties of
such systems.

Unfortunately, higher-order representation techniques are fundamentally
incompatible with the induction principles needed to reason about such
encodings.\footnote{See~\cite{Despeyroux97} for a detailed
analysis.}  In the literature three approaches have been studied in
order to overcome these problems, while retaining the advantages a
logical framework can offer.  The first called
\emph{schema-checking}~\cite{Rohwedder94proposal,Rohwedder96esop} implements
meta-theoretic proofs as relations whose operational reading as logic
programs realizes the informal proofs.  This has been applied
successfully in many case studies (see~\cite{Pfenning96caap}), but lacks
automation.  The second is based on reflection via a modal provability
operator.  At present it is unclear how this idea, developed for simple
types in~\cite{Despeyroux97}, interacts with dependent types, and if
it is flexible enough for many of the theorems that can be treated with
schema-checking.  The third is to devise an explicit (meta-)meta-logic
for reasoning about logical framework encodings.  For the simpler
logical framework of hereditary Harrop formulas this approach has been
followed by McDowell and Miller~\cite{McDowell97lics,McDowell97phd}.
However, their system suffers from the lack of dependent types and is
not directly amenable to automated deduction, since it offers only
induction over the natural numbers.\footnote{See Section~\ref{sec:rel}
for a more detailed comparison.}

In this paper we develop a simple meta-logic $\Mtwo$ for LF and sketch
its implementation in the Twelf system.  $\Mtwo$ was designed explicitly
to support automated inductive theorem proving and has been applied
successfully to prove, for example, value soundness and type
preservation for Mini-ML, completeness of a continuation stack machine
with respect to a natural semantics for Mini-ML, soundness and
completeness of uniform derivations with respect to resolution (which is
a critical step in the correctness of compilers for logic programming
languages), the deduction theorem for intuitionistic propositional logic
using Hilbert's axiomatization, and the existence of an embedding of
Cartesian closed categories into the simply-typed $\lambda$-calculus.
In each case we specified only the theorem and the induction variable,
the proof was completely automatic in every other respect.

We view Twelf as a special-purpose automated theorem prover for the
theory of programming languages and logics.  It owes its success to
the expressive power of the logical framework combined with the
simplicity of the meta-logic which nonetheless allows direct
expression of informal mathematical arguments.  Its main current
limitations are the lack of facilities for incorporating lemmas and
for proving properties which require reasoning about \emph{open} LF
objects, i.e.\ objects which may contain free variables.  We plan to
address the former by adapting standard techniques from inductive and
resolution theorem proving and the latter by borrowing successful
ideas from schema-checking.

This paper is organized as follows: In Section~\ref{sec:lf} we briefly
describe the logical framework LF and introduce a programming
language Mini-ML and a type preservation result as running example.
The meta logic $\Mtwo$ is introduced in Section~\ref{sec:meta} which
is implemented in the proof assistant Twelf which we discuss in
Section~\ref{sec:twelf}.  Section~\ref{sec:rel} compares the most
closely related work before we assess the results and discuss future
work.

\section{The Logical Framework} \label{sec:lf}

The type theory underlying the logical framework LF is an extension of
the simply-typed $\lambda$-calculus by dependent types. It also appears
under the name $\lambda P$ in Barendregt's $\lambda$-cube
\cite{Barendregt92}. It is defined by three syntactic categories of
objects, type families, and kinds \cite{Harper93jacm}.

\def\Type{\mbox{type}}
\newcommand{\abs}[2]{\lambda {#1}\!:\!{#2}.\,}
\newcommand{\Abs}[2]{\Pi {#1}\!:\!{#2}.\,}

\[\begin{array}{lccl}
  \mbox{Kinds:} & K & \bnfas & \Type \bnfalt \Abs {x}{A} K \\
  \mbox{Type Families:} & A & \bnfas & a \bnfalt A\; M \bnfalt \Abs{x}{A_1}{A_2} \\
  \mbox{Objects:} & M & \bnfas & c \bnfalt x \bnfalt \abs{x}{A}M 
  \bnfalt M_1\; M_2\\[1ex]
  \mbox{Signatures:} & \Sigma & \bnfas & \cdot \bnfalt \Sigma, a:K
  \bnfalt \Sigma,  c:A \\
  \mbox{Contexts:} & \Gamma & \bnfas & \cdot \bnfalt \Gamma, x:A 
\end{array}\]

We use $a$ for type family constants, $c$ for object constants, and $x$
for variables.  Atomic types have the form $a\; M_1\ldots M_n$ and
function types $\Abs{x}{A_1}{A_2}$, which we may write $A_1 \arrow A_2$
if $x$ does not occur free in $A_2$.  We assume that constants and
variables are declared at most once in a signature and context,
respectively.  As usual we apply tacit renaming of bound variables to
maintain this assumption and to guarantee capture-avoiding substitution.

% LF typing judgment

\newcommand {\Tp}[3]{{#1} \vdash {#2} : {#3}}
\newcommand {\Tpctx}[1]{\vdash {#1}\;\mbox{ctx}}

The LF type theory is defined by a number of mutually dependent
judgments which we will not re-iterate here.  The main typing judgment
has the form $\Gamma \vdash_{\!\Sigma} M : A$ and expresses that object
$M$ has type $A$ in context $\Gamma$ with respect to signature $\Sigma$.
We generally assume that signature $\Sigma$ is valid and fixed and
therefore omit it from the typing and other related judgments introduced
later on.  We will also need to explicitly require the validity of
contexts, written as $\Tpctx{\Gamma}$.  In a slight departure
from~\cite{Harper93jacm} we take $\beta\eta$-conversion as our notion of
definitional equality, since this guarantees that every well-typed
object has an equivalent \emph{canonical form}, that is, a long
$\beta\eta$-normal form.  The requisite theory may, for example, be
found in~\cite{Geuvers92}.

As a running example we will use Mini-ML in the formulation
of~\cite{Pfenning94un} which goes back to~\cite{Michaylov91},
culminating in an automatic proof of type preservation.  While space
only permits showing the fragment including abstraction, application,
and recursion, our automatic proof also treats the remaining features of
Mini-ML including polymorphism and an inductively defined type.

\newcommand{\Mlam}[1]{\mbox{\bf lam}\;{#1}.\,}
\newcommand{\Mapp}[1]{{#1}\mbox{{\bf @}}}
\newcommand{\Mfix}[1]{\mbox{\bf fix}\;{#1}.\,}
\def\Lexp{\mbox{exp}}
\def\Llam{\mbox{lam}}
\def\Lapp{\mbox{app}}
\def\Lfix{\mbox{fix}}

Mini-ML expressions are represented by canonical LF objects of type
$\Lexp$.  The representation function $\rep{e}$ shown below is
\emph{adequate}, that is, it is a compositional bijection between
Mini-ML expressions and canonical objects of type $\Lexp$.
Compositionality in this context means that $\rep{e[e'/x]} =
\rep{e}[\rep{e'}/x]$ and allows us to represent substitution in the
object language by $\beta$-reduction in the logical framework, since
$\rep{e}[\rep{e'}/x]$ is definitionally equal to
$(\abs{x}{\Lexp}{\rep{e}})\; \rep{e'}$.

%\begin{example}[Mini-ML]\label{ex:exp} \ \par
  \[\begin{array}{lccl}
    \mbox{Mini-ML Expressions:} & e & \bnfas & x
    \bnfalt \Mlam{x}e \bnfalt \Mapp{e_1}e_2 \bnfalt \Mfix{x}e 
  \end{array}\]
  \[ \begin{array}{rcl@{\rspace}l@{\ :\ }l} & & & \Lexp & \Type \\
    \rep{\Mlam{x}e} & = & \Llam\;(\abs{x}{\Lexp}\rep{e}) & \Llam & (\Lexp \arrow \Lexp) \arrow \Lexp \\
    \rep{\Mapp{e_1}e_2} & = & \Lapp\;\rep{e_1}\;\rep{e_2} & \Lapp & \Lexp \arrow \Lexp \arrow \Lexp \\ 
    \rep{\Mfix{x}e} & = & \Lfix\;(\abs{x}{\Lexp}\rep{e}) & \Lfix & (\Lexp \arrow \Lexp) \arrow \Lexp \\
    \rep{x} & = & x 
  \end{array} \]
%\end{example}

% Canonical forms

%\newcommand {\Can}[3]{{#1} \vdash {#2} \Uparrow {#3}}
%
%Not every well-typed object of the meta-language directly represents
%an expression of the object language. For example, we can see that
%$\rep{e}$ will never contain a $\beta$-redex. Moreover, the argument
%to $\Llam$ which has type $\Lexp \arrow \Lexp$ will always be a
%$\lambda$-abstraction. Thus the image of the translation in this
%representation methodology is always a $\beta$-normal $\eta$-long
%form. Following \cite{Harper93jacm} we call these forms canonical and
%write $\Can{\Gamma}{M}{A}$ where $\Tp{\Gamma}{M}{A}$.  Canonical forms
%are in one-to-one correspondence with the expressions we are trying to
%represent, i.e.\ the representation of expressions is adequate. 

%Canonical forms play the role of ``observable values'' in a functional
%language: they are in one-to-one correspondence with the expressions we are
%trying to represent.  For Mini-ML
%this is expressed by the following property, which is proved by simple
%inductions.
%\begin{example}[Compositional adequacy for untyped $\lambda$-expressions]
%  \label{ex:adequacy}
%  \mbox{}
%  \begin{enumerate}
%  \item Let $e$ be an expression with free variables among $x_1,\ldots, x_n$.
%    \par
%    \noindent Then $\Can{x_1:\Lexp, \ldots, x_n:\Lexp}{\rep{e}}{\Lexp}$.
%  \item Let $\Can{x_1:\Lexp,\ldots,x_n:\Lexp}{M}{\Lexp}$ 
%    \par
%    \noindent Then $M = \rep{e}$ for an expression $e$ with free variables among
%    $x_1,\ldots,x_n$.
%  \item $\rep{\cdot}$ is a bijection between expressions and canonical forms
%where  $\rep{e [e'/x]} = \rep{e}[\rep{e'}/x]$.
%  \end{enumerate}
%\end{example}

%Since every object in LF has a unique $\beta\eta$-equivalent canonical
%form, the meaning of every well-typed object is unambiguously given.


% Evaluation

%Mini-ML expressions can be evaluated operationally, a property
%which is expressible by a deductive system. We follow the
%presentation of \cite{Pfenning94un}.
 
\newcommand {\ev}[1] {{#1} \hookrightarrow}
\def\Lev{\mbox{ev}}
\def\Levlam{\mbox{ev\_lam}}
\def\Levapp{\mbox{ev\_app}}
\def\Levfix{\mbox{ev\_fix}}
\newcommand{\evLam}{\Rulefont{evLam}}
\newcommand{\evApp}{\Rulefont{evApp}}
\newcommand{\evFix}{\Rulefont{evFix}}

Expressions form the basic syntactic structure for which we define an
operational semantics and a typing discipline.  The evaluation
judgment $\ev{e}{v}$ for expressions $e$ and $v$ is defined by
the following rules of inference.

\[\begin{array}{c}
  \ianc {} {\ev {\Mlam {x} e} {\Mlam {x} e}} {\evLam} \rspace
  \ianc
  {\ev {e_1} {\Mlam {x} e_1'}
    \rspace
    \ev {e_2} {v_2}
    \rspace
    \ev {e_1' [v_2/x]} {v}}
  {\ev {\Mapp{e_1} e_2} {v}}
  {\evApp} \\[2ex]
  \ianc
  {\ev {e [\Mfix {x} e/x]} v}
  {\ev {\Mfix {x} e} {v}}
  {\evFix}
\end{array}\]
  Derivations of a judgment $\ev{e}{v}$ are represented by canonical LF
objects of type $\Lev\; \rep{e}\; \rep{v}$ over the following signature,
which means that $\Lev$ is a constant type family indexed by two
expressions.

%\[\begin{array}[t]{rcl}
%  \bigrep{\begin{array}[c]{c}
%      \ianc
%      {\above{\DD}{\ev {e [\Mfix {x} e/x]} v}}
%      {\ev {\Mfix {x} e} {v}}
%      {\evFix}
%    \end{array}}
%  &=& \Levfix\;(\abs{x}{\Lexp}\rep{e})\;\rep{v}\;\rep{\DD}.
%\end{array}\]
%The other rules are represented similarly, leading to 
%a signature of the following form:
\[ \begin{array}{lcl} 
  \Lev &:& \Lexp \arrow \Lexp \arrow \Type \\
  \Levlam &:& \Lev\; (\Llam\;{\bf E})\; (\Llam\;{\bf E}) \\
  \Levapp &:& \Lev\; (\Lapp\;{\bf E_1}\;{\bf E_2})\;{\bf V}  \\
  && \barrow\; \Lev\; {\bf E_1}\; (\Llam\;{\bf E_1'}) \\
  && \barrow\; \Lev\; {\bf E_2}\; {\bf V_2} \\
  && \barrow\; \Lev\; ({\bf E_1'}\;{\bf V_2})\; {\bf V} \\
  \Levfix &:& \Lev\; (\Lfix\; {\bf E})\;{\bf V}  \\
  && \barrow\; \Lev\; ({\bf E}\;(\Lfix\; {\bf E}))\; {\bf V}
\end{array} \]

In this example we reversed the function arrows, writing $A_2 \barrow
A_1$ instead of $A_1 \arrow A_2$ following logic programming notation.
Since $\arrow$ is right associative, $\barrow$ is left associative.  The
free variables in each declaration, written with bold uppercase names,
are implicitly $\Pi$-quantified with an appropriate type which can be
deduced from the context in which the variable appears.  For example,
the fully explicit form of the first declaration would be $\Levlam :
\Abs{E}{\Lexp \arrow \Lexp} \Lev\; (\Llam\;E)\; (\Llam\;E)$.  These
\emph{index variables} play an important role, as they must be treated
differently from other variables during proof search, as will be
discussed in Section~\ref{sec:twelf}.

%In this
%paper we refer to these variables as {\em index-variables}, because
%they are used as indices to other type families, as for example,
%$e:\Lexp \arrow \Lexp$ is an index to `$\Lev\; (\Llam\;e)\;
%(\Llam\;e)$'.

\newcommand {\Marr}[1] {{#1} \Rightarrow}
\def\Ltp{\mbox{tp}}
\def\Larr{\mbox{arr}}

Mini-ML types are denoted by $\tau$, where $\Marr{\tau_1}{\tau_2}$
stand for function types.  They are represented by canonical
LF objects of type $\Ltp$ over the (trivial) signature below.
%  \[\begin{array}{lccl}
%    \mbox{Types :} & \tau & \bnfas & a \bnfalt \Marr{\tau_1}\tau_2
%  \end{array}\]
\[ \begin{array}{rcl@{\rspace}l@{\ :\ }l} & & & \Ltp & \Type \\
  \rep{\Marr{\tau_1}\tau_2} & = & \Larr\;\rep{\tau_1}\;\rep{\tau_2}  
  & \Larr & \Ltp \arrow \Ltp \arrow \Ltp \\
\end{array} \]


\newcommand {\of}[2] {{#1} \triangleright {#2}:}
\def\Lof{\mbox{of}}
\def\Loflam{\mbox{of\_lam}}
\def\Lofapp{\mbox{of\_app}}
\def\Loffix{\mbox{of\_fix}}
\newcommand{\ofLam}{\Rulefont{ofLam}}
\newcommand{\ofApp}{\Rulefont{ofApp}}
\newcommand{\ofFix}{\Rulefont{ofFix}}

% Contexts
 %The context $\Delta$ represents implicit parameters and 
%their 

%Consider for example the rule for typing Mini-ML
%functions: To show that $\abs{x}{\tau_1}{e}$ is well-typed,
%we have to introduce a new parameter $x$ and assume its type
%to be $\tau_1$ before we can complete the well-typedness proof.

%\[\begin{array}{c}
%  \ianc{\hypo{\ian{}{\triangleright x : \tau_1}{u}} {\triangleright e:\tau_2}}
%  {\triangleright \abs{x}{\tau_1}{e} : \tau_1 \Arrow \tau_2}
%  {\ofLam^u}
%\end{array}\]

%In this paper we prefer to collect all these implicit assumptions and
%make them explicit. They form a Mini-ML context $\Delta$ which
%provides an alternative way of writing the hypothetical typing
%judgment: $$\of{\Delta}{e}{\tau}$$

We use $\Delta$ to denote Mini-ML typing assumptions for
variables in the typing judgment $\of{\Delta}{e}{\tau}$.
This is an example of a so-called \emph{hypothetical judgment},
which means that higher-order representation techniques can
be applied to great advantage.


\[\begin{array}{c}
  \ianc
  {\of {\Delta, x:\tau_1} {e} {\tau_2}}
  {\of {\Delta} {\Mlam {x} e} {\Marr {\tau_1} {\tau_2}}}
  {\ofLam} \rspace
  \ianc
  {\of {\Delta} {e_1} {\Marr {\tau_2} {\tau_1}}
    \rspace
    \of {\Delta} {e_2} {\tau_2}}
  {\of {\Delta} {\Mapp{e_1} e_2} {\tau_1}}
  {\ofApp} \\[2ex]
  \ianc
  {\of {\Delta, x:\tau} {e} {\tau}}
  {\of {\Delta} {\Mfix {x} e} {\tau}}
  {\ofFix}
\end{array}\]

A derivation of a judgment $\of{\Delta}{e}{\tau}$ is
represented by canonical LF objects of type $\Lof\; \rep{e}\; \rep{\tau}$
in an LF context $\rep{\Delta}$ which represents the Mini-ML
typing assumptions in $\Delta$ by corresponding LF typing assumption.

%\[ \Tp{\rep{\Delta}}{\rep{\PP}} {\Lof\;\rep{e}\;\rep{\tau}}\]
%where $\Delta$ is represented in the following way:
%\[\begin{array}{rcl}
%  \rep{\cdot} &=& \cdot \\
%  \rep{\Delta, x:\tau} &=& \rep{\Delta}, x : \Lexp, u: \Lof\;x\;\rep{\tau}
%\end{array}\]
%To see how the typing rules are represented, consider the rule
%$\ofFix$.  Note that also here the representation technique of
%hypothetical judgments lets us safely omit $\Delta$ from the
%representation.
%\[\bigrep{\ianc
%  {\above{\EE}{\of {\Delta, x:\tau} {e} {\tau}}}
%  {\of {\Delta} {\Mfix {x} e} {\tau}}
%  {\ofFix}} = \Loffix\;(\abs{x}{\Lexp}{\rep{e}})\;\rep{\tau}\;(\abs{x}{\Lexp} \abs{u}{\Lof\; x\;\rep{\tau}}\rep{\EE})\]
%The complete list of all new LF constants 
%representing the typing rules is given as follows.
\[ \begin{array}{lcl} 
  \Lof &:& \Lexp \arrow \Ltp \arrow \Type \\
  \Loflam &:& \Lof\; (\Llam\;{\bf E})\; (\Larr\; {\bf T_1}\; {\bf T_2}) \\
  && \barrow\; (\Abs{x}{\Lexp} \Lof\; x\; {\bf T_1} \arrow \Lof\; ({\bf E}\; x)\; {\bf T_2}) \\
  \Lofapp &:& \Lof\; (\Lapp\;{\bf E_1}\;{\bf E_2})\;{\bf T_1}  \\
  && \barrow\; \Lof\; {\bf E_1}\; (\Larr\;{\bf T_2}\; {\bf T_1}) \\
  && \barrow\; \Lof\; {\bf E_2}\; {\bf T_2} \\
  \Loffix &:& \Lof\; (\Lfix\; {\bf E})\;{\bf T}  \\
  && \barrow\; (\Abs{x}{\Lexp} \Lof\; x\; {\bf T} \arrow \Lof\; ({\bf E}\; x)\; {\bf T}) \\
\end{array} \]
 This representation is once again a compositional bijection between
Mini-ML typing derivations and canonical LF objects.  Compositionality
here means that if we have a derivation $\PP'$ of
$\of{\Delta}{e'}{\tau'}$ and a derivation $\PP$ of $\of{\Delta, x\oftp
\tau'}{e}{\tau}$, then $\PP[\PP'/X]$ is a derivation of
$\of{\Delta}{e[e'/x]}{\tau}$ and $\rep{\PP[\PP'/X]} =
\rep{\PP}[\rep{\PP'}/X]$.  Here, $X$ is a derivation variable labelling
the assumption $x\oftp\tau'$.

 Thus, compositionality of the encoding gives us the following
substitution lemma ``for free'', since it can be represented simply by
substitution in LF whose correctness has been proven once and for all
for the logical framework \cite{Harper93jacm}.

\begin{lemma} [Substitution] \label{lem:subst}
  For all contexts $\Delta$,\par
  if $\of {\Delta} {e'} {\tau'}$ and $\of {\Delta, x: \tau'} {e}
  {\tau}$ then $\of {\Delta} {e [e'/x]} {\tau}$.
\end{lemma}

A substitution lemma of this or a similar form is an important
ingredient in many theorems in logic (e.g., cut-elimination,
normalization, or the Church-Rosser theorem) or the theory of
programming languages (e.g., subject reduction or type preservation).

As a point of reference, we now give an informal proof of type
preservation for Mini-ML, which is also \emph{exactly} the proof found
automatically rendered into informal notation.  We write $\DD :: J$ if
$\DD$ is a derivation of a judgment $J$ to avoid two-dimensional
notation.  Besides structural induction, we also use \emph{inversion},
when the shape of the conclusion determines the inference rule which
must have been applied last.

\begin{theorem} [Type preservation] \label{thm:minitp}
  For all expressions $e, v$, types $\tau$, and
  derivations $\DD :: \ev{e}{v}$ and $\PP :: \of {\cdot} {e} {\tau}$,
  there exists a derivation $\QQ :: \of {\cdot} {v} {\tau}$.
\end{theorem}

\begin{proof} By structural induction over $\DD$.
  \begin{description}
  \item [Case:] $\DD = \ianc {} {\ev {\Mlam {x} e} {\Mlam {x} e}} {\evLam}$. \par
    This case is immediate because we can use $\PP$ for $\QQ$.
  \item [Case:] $\DD = \ianc {\above{\DD_1}{\ev {e_1} {\Mlam {x} e_1'}}
      \rspace
      \above{\DD_2}{\ev {e_2} {v_2}}
      \rspace
      \above{\DD_3}{\ev {e_1' [v_2/x]} {v}}}
    {\ev {\Mapp{e_1} e_2} {v}}
    {\evApp}$. \par
    We have $\PP :: \of {\cdot} {\Mapp{e_1} e_2} {\tau}$. By 
    inversion, we obtain 
    $\PP_1 :: \of {\cdot} {e_1} {\Marr {\tau_2} {\tau}}$ and 
    $\PP_2 :: \of {\cdot} {e_2} {\tau_2}$ for some $\tau_2$.
    By induction hypothesis on $\DD_1$ and $\PP_1$ we obtain 
    $\QQ_1 :: \of {\cdot} {\Mlam {x} e_1'} {\Marr {\tau_2} {\tau}}$.
    Another inversion step gives us 
    that $\QQ_1' :: \of{x:\tau_2}{e_1'}{\tau}$. A second appeal
    to the induction hypothesis on $\DD_2$ and $\PP_2$ yields
    that $\QQ_2 :: \of{\cdot}{v_2}{\tau_2}$. The application of the
    substitution lemma gives us a $\QQ_2' :: \of{\cdot}{e'_1[v_2/x]}{\tau}$.
    Finally, applying the induction hypothesis to $\DD_3$ and $\QQ_2'$
    results in the required derivation $\QQ_3 :: \of{\cdot}{v}{\tau}$.
    
  \item [Case:] $\DD = \ianc
    {\above{\DD_1}{\ev {e [\Mfix {x} e/x]} v}}
    {\ev {\Mfix {x} e} {v}}
    {\evFix}$. \par
    We have $\PP :: \of {\cdot} {\Mfix {x} e} {\tau}$. By 
    inversion we immediately obtain a 
    $\PP_1 :: \of {x:\tau} {e} {\tau}$. Applying the substitution
    lemma yields $\PP_1' :: \of{\cdot}{e [\Mfix {x} e/x]}{\tau}$. By applying
    the induction hypothesis to $\DD_1$ and $\PP_1'$ we obtain 
    the desired derivation $\QQ_1 :: \of {\cdot}{v}{\tau}$.
  \end{description}
\end{proof}

\def\tps{\mbox{tps}} \def\babs{\mbox{abs}} 

How can we render this informal proof in a formal system?  The proof is
clearly constructive and contains a method for constructing a derivation
$\QQ:: \of{\cdot}{v}{\tau}$ from $\DD::\ev{e}{v}$ and
$\PP::\of{\cdot}{e}{\tau}$.  By an extension of the Curry-Howard
correspondence one might hope to represent this as an LF function
 \[ \tps : \Lev\;{\bf E}\;{\bf V} \arrow \Lof\;{\bf E}\;{\bf T} \arrow
\Lof\;{\bf V}\;{\bf T}. \]
 In fact, if we could exhibit a total function of this type, we would
know that type preservation holds.  Unfortunately, such a function does
not exist in LF, since it would have to be defined by primitive
recursion over its first argument, and primitive recursion is not
available in LF\@.  Moreover, straightforward attempts to add primitive
recursion render higher-order representations inadequate.  This is
discussed in detail in~\cite{Despeyroux97}.

Instead we define a meta-logic for LF in which it is possible to
express and prove:
 \begin{quote}
  For all closed LF objects $E:\Lexp$, $V:\Lexp$, $T:\Ltp$,
$D:\Lev\; E\; V$, and $P:\Lof\;E\;T$
there exists a closed LF object $Q:\Lof\; V\; T$.
 \end{quote}
% \begin{quote}
%  For all closed LF objects ${\bf E}:\Lexp$, ${\bf V}:\Lexp$, ${\bf T}:\Ltp$,
%$D:\Lev\; {\bf E}\; {\bf V}$, and $P:\Lof\;{\bf E}\;{\bf T}$
%there exists a closed LF object $Q:\Lof\;{\bf V}\;{\bf T}$.
% \end{quote}
 By the adequacy of the encodings, the existence of such an LF object
 $Q$ means the existence of a typing derivation $\QQ$ of
 $\of{\cdot}{v}{\tau}$, where $\rep{v} = V$ and $\rep{\tau} = T$,
 guaranteeing the type preservation property for Mini-ML.

\section{Meta-Logic $\Mtwo$} \label{sec:meta}

% Language

\newcommand{\AllA}[1]{\forall {#1}.\,}
\newcommand{\ExA}[1]{\exists {#1}.\,}
\newcommand{\All}[2]{\forall {#1}\!:\!{#2}.\,}
\newcommand{\Ex}[2]{\exists {#1}\!:\!{#2}.\,}
\newcommand{\And}[1]{{#1} \wedge}
\newcommand{\True}{\top}

The purpose of the meta-logic $\Mtwo$ is formal reasoning about
properties of LF signatures, with the goal of automating the proof
of such properties.  Since LF signatures implement object languages
and their semantics, this provides for automatic proofs of
properties of logics and programming languages.

$\Mtwo$ is a restricted constructive first-order logic where quantifiers
range over closed LF objects constructed over a given signature
$\Sigma$.  Its formal definition is a sequent calculus endowed with
realizing proof terms.

The formal system of $\Mtwo$ in its full generality is rather complex.
We therefore present here only a restriction of $\Mtwo$, where pattern
matching subjects must be of atomic type. For a complete presentation of
the meta logic we refer the interested reader to the detailed
forthcoming technical report \cite{Schuermann98tr}. We introduce $\Mtwo$
in four steps: in Section~\ref{sec:intlogic} we describe a
constructive logic over LF which we augment with proof terms in
Section~\ref{sec:pterms} and by well-founded recursion in
Section~\ref{sec:rec}.  In Section~\ref{sec:case} we introduce
definition by cases and in Section ~\ref{sec:metatheory} we establish
the necessary meta-theoretic properties of $\Mtwo$ which make it an
appropriate meta-logic.

% Judgments

\newcommand{\IC}[3]{{#1};{#2} \vdash  {#3}}
\newcommand{\ICP}[4]{{#1};{#2} \vdash {#3} \in {#4}}
\newcommand{\TPR}[3]{{#1} \vdash {#2} \in {#3}}
\newcommand{\TP}[5]{{#2};{#3} \vdash {#4} \in {#5}}
\newcommand{\TPC}[7]{{#2};{#3} \vdash_{#4}\; {#6} \in {#7}}


\newcommand{\vv}{{\mathbf v}}
\newcommand{\xx}{{\mathbf x}}
\newcommand{\yy}{{\mathbf y}}
\newcommand{\zz}{{\mathbf z}}
\newcommand{\all}[2]{\Lambda {#1}\!:\!{#2}.\,}
\newcommand{\allA}[1]{\Lambda {#1}.\,}
\newcommand{\exA}[1]{\langle {#1}\rangle}
\newcommand{\rec}[2]{\mu {#1}\in{#2}.\,}
\newcommand{\inx}[2]{[{#1}, {#2}]}
\newcommand{\pair}[2]{\langle {#1}, {#2}\rangle}
\newcommand{\unit}{\langle\rangle}
\newcommand{\split}[2]{\mbox{split}\;{#1}\;\mbox{as}\;\langle {#2} \rangle\;\mbox{in}\;}
\newcommand{\caseA}[1]{\mbox{case}\;{#1}\;\mbox{of}\;}
\newcommand{\select}[3] {({#1} \triangleright {#2} \mapsto {#3})}
\newcommand{\selectA}[2] {{#1} \triangleright {#2} \mapsto}
\newcommand{\letvar}[2]{\mbox{let}\;{#1} = {#2}\;\mbox{in}\;}

% Abbreviations

\newcommand{\absA}[1]{\lambda  {#1}.\,} 
\newcommand{\AbsA}[1]{\Pi {#1}.\,}
\newcommand {\id}[1]{\mbox {id}_{#1}}
\newcommand{\restrict}[1]{|_{#1}}


% Typing rules

\newcommand{\axunit}{\Rulefont{axunit}}
\newcommand{\axvar}{\Rulefont{axvar}}
\newcommand{\axfixvar}{\Rulefont{axfixvar}}
\newcommand{\fix}{\Rulefont{fix}}
\newcommand{\nofix}{\Rulefont{nofix}}
\newcommand{\forallL}{\Rulefont{$\forall$L}}
\newcommand{\forallR}{\Rulefont{$\forall$R}}
\newcommand{\existsL}{\Rulefont{$\exists$L}}
\newcommand{\existsR}{\Rulefont{$\exists$R}}
\newcommand{\andL}{\Rulefont{$\wedge$L}}
\newcommand{\andR}{\Rulefont{$\wedge$R}}
\newcommand{\objectL}{\Rulefont{case}}
\newcommand{\sigempty}{\Rulefont{sigempty}}
\newcommand{\siguni}{\Rulefont{siguni}}
\newcommand{\signonuni}{\Rulefont{signonuni}}
\newcommand{\ctxuni}{\Rulefont{ctxuni}}
\newcommand{\ctxnonuni}{\Rulefont{ctxnonuni}}
\newcommand{\structw}{\Rulefont{structW}}
\newcommand{\structc}{\Rulefont{structC}}
\newcommand{\structx}{\Rulefont{structX}}
\newcommand{\subid}{\Rulefont{subId}}
\newcommand{\subdot}{\Rulefont{subDot}}

\subsection{A Constructive Sequent Calculus Over LF} \label{sec:intlogic}

Formulas in $\Mtwo$ have the form $\All{x_1}{A_1} ... \All{x_n}{A_n}
\Ex{y_1}{B_1} ... \Ex{y_m}{B_m} \True$ (which we write as
$\AllA{\Gamma_1} \ExA{\Gamma_2} \True$, where $\Gamma_1 = x_1 : A_1,
..., x_n :A_n$ and $\Gamma_2 = y_1:B_1, ..., y_m: B_m$).  Here all $A_i$
and $B_j$ are LF types, and for a formula to be well-formed the combined
context $\Gamma_1, \Gamma_2$ must be a valid LF context.

While this may not seem very expressive, it is sufficient for many
theorems in the realm of logic and the theory of programming languages
we have examined, since other connectives (such as disjunction) and even
more complex quantifier alternations can be incorporated at the level of
LF\@.  The main limitation is that the quantifiers range only over
closed LF objects of the given types; a generalization is the subject of
current research.

\[\begin{array}{lccl}
  \mbox{\it Formulas} & F & \bnfas &  \AllA {\Gamma_1} \ExA {\Gamma_2} \True \\
  \mbox{\it Assumptions} & \Delta & \bnfas & \cdot \bnfalt \Delta, F
\end{array}\]

The judgment for provability for this sequent calculus is
$\IC{\Gamma}{\Delta}{F}$, where the LF context $\Gamma$ makes all
Eigenvariables explicit with their type.  The judgment is also indexed
by an LF signature $\Sigma$ which we suppress for the sake of brevity.

\begin{figure}[t]
  \begin{center} \footnotesize 
    \begin{tabular}{|c|}
      \hline
      $\begin{array}{cc}
        \ianc{\Tp{\Gamma}{\sigma}{\Gamma_1} \rspace
          \IC{\Gamma}{\Delta_1,  \AllA {\Gamma_1} F_1, \Delta_2, F_1 [\sigma]}{F_2}}
        {\IC{\Gamma}{\Delta_1, \AllA {\Gamma_1} F_1, \Delta_2}{F_2}}{\forallL} 
        &
        \ianc{\IC{\Gamma, \Gamma_1}{\Delta}{F}}
        {\IC{\Gamma}{\Delta}{\AllA {\Gamma_1} F}}{\forallR^*} \\[2ex]
        \ianc{\IC{\Gamma, \Gamma_1}{\Delta_1, \ExA {\Gamma_1} \True, \Delta_2}{F}}
        {\IC{\Gamma}{\Delta_1, \ExA {\Gamma_1} \True, \Delta_2}{F}}{\existsL^*} 
        &
        \ianc{\Tp{\Gamma}{\sigma}{\Gamma_1}}
        {\IC{\Gamma}{\Delta}{\ExA {\Gamma_1} \True}}{\existsR} \\[2ex]
        \multicolumn{2}{@{^*\;}l}{\mbox{Eigenvariable condition: $\Tpctx{\Gamma, \Gamma_1}$}}
      \end{array}$ \\
      \hline 
    \end{tabular}
  \end{center}
  \caption {Constructive Logic Over LF}
  \label{fig:intlogic}
\end{figure}

The rules for the judgment are in the form of a sequent calculus and
defined in Figure~\ref{fig:intlogic}.  Because of the way our search
engine actually works and the restriction on quantifier alternations, it
is convenient to instantiate all quantified variables of the same kind
simultaneously by means of a substitution $\sigma$ explained below.
This applies to the $\forallL$ and $\existsR$ rules, where the latter
also incorporates an axiom rule for $\True$.

\[\begin{array}{lccl}
  \mbox{\it Substitutions} & \sigma & \bnfas & \cdot
    \bnfalt \sigma, M/x
\end{array}\]

Valid substitutions map variables in a context $\Gamma'$ to
valid objects in a context $\Gamma$.  This judgment is written
as $\Tp{\Gamma}{\sigma}{\Gamma'}$ and defined by the following
inference rules, which guarantees that dependencies are properly
respected.

\[\begin{array}{cc}
  \ianc{}
  {\Tp{\Gamma}{\cdot}{\cdot}}
  {\subid}
  \rspace
  \ianc{\Tp{\Gamma}{\sigma}{\Gamma'} \rspace \Tp{\Gamma}{M}{A[\sigma]}}
  {\Tp{\Gamma}{(\sigma, M/x)}{(\Gamma', x:A)}}
  {\subdot}
\end{array}\]

When $\Tp{\Gamma}{\sigma}{\Gamma'}$ and $\Tp{\Gamma'}{M}{A}$ then we
write $M[\sigma]$ for the result of applying the substitution $\sigma$
to $M$, and similarly for types, contexts, etc.  The result will satisfy
$\Tp{\Gamma}{M[\sigma]}{A[\sigma]}$.  This is also reflected in our
implementation of the system, which employs dependently typed explicit
substitutions.

We write $\id{\Gamma}$ for the identity substitution on $\Gamma$ satisfying
$\Tp{\Gamma}{\id{\Gamma}}{\Gamma}$.  The formulation of the calculus
incorporates the structural rules: weakening is implicit in
$\existsR$, contraction and exchange are implicit in the left rules
$\forallL$ and $\existsL$.

The type preservation theorem (Theorem~\ref{thm:minitp}) can be
expressed in $\Mtwo$ as
   \[ \AllA {E:\Lexp, V:\Lexp,
  T:\Ltp, D:\Lev\;E\;V, P:\Lof\;E\;T} \ExA
  {Q:\Lof\;V\;T} \True \]
 Using our implicit index variable convention, this may be abbreviated
to $\AllA {D:\Lev\;{\bf E}\;{\bf V}, P:\Lof\;{\bf E}\;{\bf T}} \ExA
{Q:\Lof\;{\bf V}\;{\bf T}} \True$.

\subsection{Adding Proof Terms} \label{sec:pterms}

%For example
%the Curry-Howard isomorphism shows, that the simply-typed
%$\lambda$-calculus provides proof terms for the natural deduction
%calculus. The existence of this isomorphism relies on the fact that
%the simply-typed $\lambda$-calculus is strongly normalizing, and hence 
%proof terms of natural deductions always correspond to total functions.

$\Mtwo$ extends the calculus in Figure~\ref{fig:intlogic} by proof terms
denoted by $P$.  Assumptions now have the form $\xx \in F$, where $\xx$
is a new kind of variable ranging over proof terms (which must not be
confused with LF variables).  The provability judgment then has the form
$\ICP{\Gamma}{\Delta}{P}{F}$ where $P$ is a proof term for $F$ and the
assumptions in $\Delta$ are now labelled.

The result of endowing all inference rules from
Figure~\ref{fig:intlogic} with proof terms is given in
Figure~\ref{fig:TP}. Every inference rule introduces a new proof term
constructor.  The proof terms for the $\forallR$ and the $\existsR$
rule are `$\allA{\Gamma_1} P$' (simultaneous abstraction over several
binders) and `$\exA{\sigma}$' (witnessing substitution), respectively.
Symmetrically, the proof terms for the $\forallL$ and the $\existsL$
rule are `$\letvar{\yy}{\xx\;\sigma}P$' (simultaneous application of
$\xx$ to the LF-objects in $\sigma$) and `$\split{\xx}{\Gamma_1} P$'
(binding variables in $\Gamma_1$ to objects of a substitution,
represented by $\xx$), respectively.


\begin{figure}[t]
  \begin{center} \footnotesize 
    \begin{tabular}{|c|}
      \hline
      $\begin{array}{cc}
        \ianc{\Tp{\Gamma}{\sigma}{\Gamma_1} \rspace
          \ICP{\Gamma}{\Delta_1,  \xx \in \AllA {\Gamma_1} F_1, \Delta_2, \yy \in F_1 [\sigma]}{P}{F_2}}
        {\ICP{\Gamma}{\Delta_1, \xx \in \AllA {\Gamma_1} F_1, \Delta_2}{\letvar{\yy}{\xx\;\sigma}{P}}{F_2}}{\forallL} 
        &
        \ianc{\ICP{\Gamma, \Gamma_1}{\Delta}{P}{F}}
        {\ICP{\Gamma}{\Delta}{\allA{\Gamma_1} P}{\AllA {\Gamma_1} F}}{\forallR^*} \\[2ex]
        \ianc{\ICP{\Gamma, \Gamma_1}{\Delta_1, \xx \in \ExA {\Gamma_1} \True, \Delta_2}{P}{F}}
        {\ICP{\Gamma}{\Delta_1, \xx \in \ExA {\Gamma_1} \True, \Delta_2}{\split{\xx}{\Gamma_1} P}{F}}{\existsL^*} 
        &
        \ianc{\Tp{\Gamma}{\sigma}{\Gamma_1}}
        {\ICP{\Gamma}{\Delta}{\exA {\sigma}}{\ExA {\Gamma_1} \True}}{\existsR} \\[2ex]
        \multicolumn{2}{@{^*\;}l}{\mbox{Eigenvariable condition: $\Tpctx{\Gamma, \Gamma_1}$}}
      \end{array}$ \\
      \hline 
    \end{tabular}
  \end{center}
  \caption{$\Mtwo$ without recursion or pattern matching}
  \label{fig:TP}
\end{figure}
 
%The proof terms of $\Mtwo$ form the following language.
%\[\begin{array}{lccl}
%  \mbox{Proof terms:} & P & \bnfas & 
%    \allA {\Gamma} P \bnfalt \exA {\sigma} \bnfalt \letvar {\yy}{\xx\ \sigma}{P}
%     \bnfalt \split{\xx}{\Gamma} P
%\end{array}\]

%\begin{example}[Using $\tps$]
%  Let $d$ be the representation of the evaluation derivation
%  $\rep{\ev{\Mapp {\Mlam {x} x} {\Mlam {y} y}}{\Mlam {y} y}}$ 
%  %is $\Levapp\;\Levlam\;\Levlam\;\Levlam$, 
%  and $p$ the representation of the typing derivation of $\rep {\of
%    {\cdot}{\Mapp {\Mlam {x} x} {\Mlam {y} y}} {\Marr{\tau}{\tau}}}$.
%%  $\Lofapp\;(\Loflam\; \abs{x}{\Lexp}\abs{P}{\Lof\;x\;T} P)
%%  \;(\Loflam\;\abs{x}{\Lexp}\abs{P}{\Lof\;x\;(\Larr\;T\;T)} P)$
%  A proof term representing the typing derivation of $\rep{\of{}{\Mlam
%      {y} y}{\Marr{\tau}{\tau}}}$ can be obtained by applying the
%  proof term realizing the type preservation proof:
%  \[\begin{array}{l}
%    \cdot;\xx \in \AllA {D:\Lev\;{\bf E}\;{\bf V},  
%      P:\Lof\;{\bf E}\;{\bf T}} \ExA {Q:\Lof\;{\bf V}\;{\bf T}} \True \\
%    \vdash \letvar {\yy}{\xx\;(\cdot, p/P, d/D)} \split{\yy}{q} \exA{q/Q} :  
%    \AllA{\cdot}\ExA {Q:\rep{\of{}{\Mlam {y} y}{\Marr{\tau}{\tau}}}} \True
%  \end{array}\]
%\end{example}

The system presented in Figure~\ref{fig:TP} is the core of the meta logic
$\Mtwo$ for LF\@.  In the next two sections we strengthen $\Mtwo$ by
introducing well-founded recursion and definition by cases for closed LF
objects.  This will allow us to represent many proofs by structural
induction, case distinction, and inversion in $\Mtwo$.  A further
extension of $\Mtwo$ is the introduction of conjunction as formula and
corresponding pairs as proof terms. These constructs are required for
the representation of mutual inductive proofs, but omitted here for the
sake of brevity (see \cite{Schuermann98tr}).

\subsection{Adding Recursion} \label{sec:rec}

The recursion operator $\rec{\xx}{F}{P}$ is the standard fixed point operator
at the level of proof terms with the following introduction rule.
\[\begin{array}{c}
  \ianc{\TP{\Psi}{\Gamma}{\Delta, \xx \in F}{P}{F}}
  {\TP{\Psi}{\Gamma}{\Delta}{\rec{\xx}{F}P}{F}}{\fix     
    \;\;\;\;\mbox{(where $\rec{\xx}{F}{P}$ terminates in $\xx$)}}
\end{array}\]

%The inference rule introduces the recursion operator on the level of
%proof terms, very similar to the typing rule `$\Loffix$' in Mini-ML in
%Section~\ref{sec:lf}. The reader should be cautious not to confuse
%both operators.

It is obvious that a proof term represents a total function only if it
terminates independently of the arguments it is applied to.  Thus the
side condition on the rule.  For termination we use arbitrary
lexicographic extensions of the subterm ordering on LF objects
described in~\cite{Rohwedder96esop}, all of which are well-founded
orderings and easy to check due to the restricted nature of our
meta-logic.

%We guarantee termination for all proof terms in $\Mtwo$ 
%by extending the termination ordering introduced by Rohwedder
%and Pfenning \cite{Rohwedder96esop} to a lexicographical termination
%ordering. The arguments to a recursive call must decrease according to
%this termination ordering. We use this idea to define a well-founded
%ordering on environments with respect to the recursion variable:
%$\gamma \prec_{\xx} \gamma'$. We say that $\rec{\xx}{F}{P}$ terminates
%in $\xx$ iff for all environments $\gamma$ and for all subterms
%`$\letvar{\yy}{\xx\;\sigma}P'$' of $P$ the following holds: $\gamma,
%\sigma \prec_{\xx} \gamma$. For example in the proof of the type preservation
%theorem, let $D^{(n)}$ the induction variable during the $n$-th recursive
%call and $D^{(n+1)}$ the variable during the next. Then for all environments
%$\gamma$, $\gamma (D^{(n)}) \prec \gamma, \sigma (D^{(n+1)})$ according
%to the subterm ordering.

\subsection{Adding Case Analysis} \label{sec:case}

The context of Eigenvariables $\Gamma$ in the judgment
$\ICP{\Gamma}{\Delta}{P}{F}$ represents all LF variables which might
occur free in the proof term $P$.  Because of the assumption that
proof terms are only applied to closed LF objects, i.e.\ objects that
do not contain any free variables, all variables in $\Gamma$ stand for
closed LF objects. It is therefore possible to determine all possible
cases for the top-level constructor of such objects.

Assume we would like to distinguish all possible cases for a given
LF variable $x$ of type $A$ declared in $\Gamma$.  For simplicity, we
assume that $A$ is a base type, even though in the full
system~\cite{Schuermann98tr} function types are also permitted which
is needed, for example, in the proof of the deduction theorem.  The
top-level structure of a closed canonical term of base type is always
$c\; x_1\ldots x_n$, where $x_i$ are new
variables\footnote{technically, they may need to be $\eta$-expanded}.
If $c$ has type $\Abs{x_1}{A_1}{\ldots\Abs{x_n}{A_n}{B}}$, then this
is a possible candidate for the shape of $x:A$ if $B$ unifies with
$A$.

This idea is very similar to the realization of partial inductive
definitions and definitional reflection~\cite{SchroederHeister93lics},
except that dependent types can eliminate more cases statically.  Also,
because of the higher-order nature of the term language, we need to deal
with the undecidability of the full higher-order unification problem.
Our solution is to restrict the analysis of possible cases to Miller's
higher-order patterns, generalized to the setting of dependent
types~\cite{Pfenning91lics}.  However, we do not restrict our system to
patterns statically, since this would preclude, for example, the direct
appeal to substitution or substitution lemmas at the level of LF\@.
Instead, we simply rule out definition by cases where determining the
possible cases would require unification beyond the pattern fragment.

Formally, we extend the language of proof terms by a case construct.
\[\begin{array}{lccl}
  \mbox{\it Patterns} & R & \bnfas & 
  \Gamma'; \Gamma'' \triangleright M \\
  \mbox{\it Cases} & \Omega & \bnfas & \cdot
    \bnfalt \Omega, R \mapsto P \\
  \mbox{\it Proof Terms} & P & \bnfas & ... \bnfalt \caseA{x}{\Omega}  \\
\end{array}\]
 The objects $M$ in patterns are strongly restricted by the rules which
check valid patterns; usually it will be a constant applied to
variable arguments, but because of dependencies, it might be more
complex than that.  Contexts $\Gamma'$ and $\Gamma''$ are separated for
technical reasons, where $\Gamma'$ contains the variables which will
be instantiated when the case subject is matched against the object $M$, while
$\Gamma''$ contains those variables which will not be instantiated (although
their types could still be instantiated).  We always have that
$\Tp{\Gamma',\Gamma''}{M}{A'}$ for some type $A'$ which is equal to
or more specific than the type $A$ of the case subject $x$.

The judgment for checking the validity of a case construct has the form
$\TPC{\Psi}{\Gamma_1;
x:B_x;\Gamma_2}{\Delta}{\Sigma}{\Gamma_S}{\Omega}{F}$, where we maintain
the invariant that $B_x$ depends on all variables in $\Gamma_1$, which
therefore collects the variables which will be instantiated by pattern
matching.  By using the limited permutation properties of
LF~\cite{Harper93jacm} this can always be established.  The following
rule then completes the definition of derivability in $\Mtwo$.
\[\begin{array}{c}
  \ianc{\Gamma (x) =  B_x
    \rspace \TPC{\Psi}{\Gamma_1; x : B_x; \Gamma_2}{\Delta}{\Sigma}{\Gamma_x}
    {\Omega}{F}}
  {\TP{\Psi}{\Gamma}{\Delta}{\caseA{x}\Omega}{F}}{\objectL} 
\end{array}\]
 where $\Gamma_1, x:B_x, \Gamma_2$ is a valid permutation of $\Gamma$,
and $B_x$ depends on all variables in $\Gamma_1$.  The judgment
$\TPC{\Psi} {\Gamma_1;x:
B_x;\Gamma_2}{\Delta}{\Sigma}{\Gamma_S}{\Omega}{F}$ selects all
constants from $\Sigma$ which are possible shapes of a closed
object of type $B_x$.  The rules for the judgment are given in
Figure~\ref{fig:TPC}.  This judgment iterates through the signature
$\Sigma$, trying each constant $c$ in turn.  If the target type $B_c$
unifies with the type $B_x$ of the case subject ($\siguni$), 
a new case is added to $\Omega$.  Otherwise, $c$ cannot be a top-level constructor for a closed
term $M$ of type $B_x$ and no case is added ($\signonuni$). 

For the description of the rules we use $\AbsA{\Gamma_c}{B_c}$ to
describe the combination of several abstractions and assume $B_c$ is
atomic.  We write $c\;\Gamma_c$ for the result of applying $c$ to the
variables in $\Gamma_c$ in order, which gives us the most general form
of a term in canonical form whose head is $c$.

The first side condition of $\siguni$ determines the substitution
$\sigma$, which instantiates all occurring variables in the $B_x$
(namely $\Gamma_1$) by objects which are defined in a new context
$\Gamma'$.  Moreover, $\sigma$ instantiates $x$ by $c\;\Gamma_c$. The
second side condition extends $\sigma$ to a substitution $\sigma'$
which acts on $\Gamma_1, x:\AbsA{\Gamma_x}{B_x}$ as $\sigma$, and on
$\Gamma_2$ as the identity.

\newcommand{\unify}[1]{\mbox{mgu}\;({#1})}
% \newcommand{\match}[1]{\mbox{match}\;({#1})}
\newcommand {\dummy}{\rule[-.1cm]{0cm}{.5cm}}

\begin{figure}[t]
  \begin{center} \footnotesize 
    \begin{tabular}{|cc|}
      \hline
      
%sigempty
      \multicolumn{2}{|c|}
      {$\ianc{}
      {\TPC{\Psi} {\Gamma_1; x:B_x; \Gamma_2}{\Delta}{\cdot}{\cdot}
        {\cdot}{F}}
      {\dummy\sigempty} 
      $} \\[1ex]

% signonuni
      \multicolumn{2}{|c|}
      {$\ianc{\TPC{\Psi} {\dummy\Gamma_1;x:B_x;\Gamma_2}{\Delta}{\Sigma}{\cdot}
        {\Omega}{F}}
      {\TPC{\Psi} {\Gamma_1;x: B_x;\Gamma_2}{\Delta}{\Sigma, 
          c:\AbsA{\Gamma_c}{B_c}}{\cdot}{\Omega}{F}}
      {\signonuni\ \ \begin{array}{l}(B_x, B_c\;
          \mbox{do not unify})
        \end{array}}$} \\[2ex]

      \multicolumn{2}{|c|}
      {$\begin{array}{c}
          \ianc{\TP{\Psi}{\dummy\Gamma', \Gamma_2[\sigma]}{\Delta [\sigma']}{P}{F [\sigma']} \rspace
            \TPC{\Psi} {\Gamma_1;x: B_x;\Gamma_2}{\Delta}{\Sigma}{\cdot}
            {\Omega}{F}}
          {\TPC{\Psi} {\Gamma_1;x:  B_x;\Gamma_2}{\Delta}{\Sigma, 
              c:\AbsA{\Gamma_c}{B_c}}{\cdot}
            {\Omega, \select {\Gamma';\Gamma_2[\sigma]}{(c\;\Gamma_c)[\sigma]}{P}}{F}}
          {\siguni} 
          \\[2ex]
          \begin{array}{r@{\;}c@{\;}l}
            \Gamma' \vdash \sigma &=& 
            \unify{B_x \doteq B_c,
              x \doteq c\; \Gamma_c} : (\Gamma_1, x:B_x, \Gamma_c) \\
            \Gamma', \Gamma_2[\sigma] \vdash \sigma' &=& (\sigma, \id{\Gamma_2}) : (\Gamma_1, x:B_x, \Gamma_c, \Gamma_2)
          \end{array}
        \end{array}$} \\
      \hline
    \end{tabular}
  \end{center}
  \caption{Selection rules for $\TPC{\Psi} {\Gamma_1;x: B_x;\Gamma_2}
    {\Delta}{\Sigma}{\Gamma_S}{\Omega}{F}$}
  \label{fig:TPC}
\end{figure}

\subsection {Properties of $\Mtwo$} \label{sec:metatheory}
\newcommand {\State}[4]{{#1};{#2};{#3} \triangleright {#4}}
\newcommand {\evalsto}{ \stackrel{*}{\Longrightarrow}}
\newcommand {\goesto}{\Longrightarrow}
 
The principal property of $\Mtwo$ which justifies its use
for reasoning about closed LF objects is the following.
\begin{theorem}
 If $\ICP{\cdot}{\cdot}{P}{\AllA{\Gamma_1}{\ExA{\Gamma_2}{\True}}}$ is
derivable for some $P$, then for every closed substitution
$\Tp{\cdot}{\sigma_1}{\Gamma_1}$ there exists a substitution
$\Tp{\cdot}{\sigma_2}{\Gamma_2[\sigma_1]}$.
 \end{theorem}

As indicated at the end of Section~\ref{sec:lf}, this, together with the
adequacy of the encodings guarantees the meta-theoretic properties of
the object languages we can express in $\Mtwo$.  Note that this is
different from and in many ways simpler than a full cut-elimination
result for $\Mtwo$.

The proof of this central property is non-trivial.  What we
show is that the realizing proof terms $P$ can be used to calculate
$\sigma_2$ from $\sigma_1$.  For this purpose, we define a small-step,
call-by-value, continuation-passing operational semantics for proof terms $P$
with explicit environments and establish the following three properties.
 \begin{description}
  \item[Type Soundness:] each step in the evaluation of $P$ preserves types
and provability in $\Mtwo$ (the critical idea here is the use of explicit
environments rather than substitution, since substitution may render
some branches in a case distinction inapplicable, thereby invalidating it),
  \item[Progress:] at each step we either have a final result, or a rule
in the operational semantics applies (the critical step here shows that
all possibilities are covered in a definition by cases);
  \item[Termination:] all reduction sequences terminate (the critical step
here uses well-foundedness restriction on recursion).
 \end{description}
 Unfortunately, space does not permit us to show the details of this
proof or even the definition of the operational semantics.  The interested
reader is referred to~\cite{Schuermann98tr}.

\section{Twelf} \label{sec:twelf}

Twelf is a theorem prover for LF which directly implements the
meta-logic $\Mtwo$ (including mutual induction and distinction by cases
over functions).  It provides an interactive mode for experimentation
and an automatic mode in which only the theorem and the termination
ordering are specified.  The deduction engine implements only a few
elementary operations, which are used to formalize the four important
basic proof principles: inversion (that is, determining all possible
shapes of an LF object from its type), direct proofs (that is, direct
construction of an LF object), and appeals to the induction hypothesis.
The interactive mode also supports lemma application.

\subsection{Elementary Operations}

We discuss the elementary operations using the proof of
the type preservation theorem as an example.  The initial goal
\[ \AllA{D:\Lev\;{\bf E}\;{\bf V}, P:\Lof\;{\bf E}\;{\bf T}} \ExA
{Q:\Lof\;{\bf V}\;{\bf T}} \True \]
 and the induction principle (induction over $D$) are specified by the
user.  Twelf uses only outermost induction, so there is an implicit
application of the recursion rule before the real proof process is
started.  Then Twelf generates subgoals by applying its elementary
operations until all subgoals are solved, using the strategy described
in the next section.

The most basic step is directly constructing a substitution for the
existentially quantified variables using the constants from the
signature and the universally quantified variables.  We call this step
{\em filling}.  It is basically a straightforward, iterative-deepening
search over an LF signature and is derived from a related implementation
of resolution for logic programming~\cite{Pfenning94cade}.

Such a substitution does not exist for the current state, so the system
applies the {\em splitting} operation which performs a case analysis as
part of the induction principle: it inspects the signature for possible
``shapes'' of $D$ and generates in our example a list of three subgoals,
automatically updating the context of universal variables.

\begin{description}
\item [Subgoal:] $\Levlam$: 
  \[\AllA{P:\Lof\;(\Llam\; {\bf E})\; {\bf T}} \ExA {Q:\Lof\;(\Llam\; {\bf E})\; {\bf T}} \True \]
\item [Subgoal:] $\Levapp$:
  \[\begin{array}{c}
    \forall D_3:\Lev\;({\bf E_1'}\;{\bf V_2})\;{\bf V},\; D_2:\Lev\;{\bf E_2}\;{\bf V_2}, D_1:\Lev\;{\bf E_1}\;(\Llam\;{\bf E_1'}), \\
     \rspace P:\Lof\;(\Lapp\;{\bf E_1}\;{\bf E_2})\;{\bf T}.\, \ExA {Q:\Lof\;{\bf V}\;{\bf T}}\True
  \end{array}\]
  \item [Subgoal:] $\Levfix$:
  \[\AllA{D_1:\Lev\;({\bf E}\;(\Lfix\;{\bf E}))\;{\bf V},
     P:\Lof\;(\Lfix\;{\bf E})\;{\bf T}}\ExA{Q:\Lof\;{\bf V}\;{\bf T}} \True\]
\end{description}

For the sake of brevity, we skip the discussion of the first two
subgoals, and continue with the third.  Inversion is now applied to $P$
in the informal proof.  In Twelf inversion is realized by another
splitting operation which generates only one subgoal in this
example. The other two potential cases ($\Loflam$, $\Lofapp$) are
rejected by Twelf, because their types are incompatible with the type of
$P$.  This leaves the subgoal
\[\AllA{D_1:\Lev\;({\bf E}\;(\Lfix\;{\bf E}))\;{\bf V},\;
    P_1:\Abs{x}{\Lexp}\;\Lof\;x\;{\bf T} \arrow\Lof\;({\bf E}\;x)\;{\bf T}}
  \ExA {Q:\Lof\;{\bf V}\;{\bf T}} \True.
\]
 Note, that in this goal the variable $P_1$ is functional and represents
a hypothetical derivation.

It is now possible to appeal to the induction hypothesis in an operation
we call {\em recursion}.  The termination condition of the $\fix$-rule
requires that it is only applied to a term smaller than $D =
\Levfix\;D_1$. According to the termination ordering in
\cite{Rohwedder96esop} there is only one possibility, namely $D_1$.

We cannot appeal to the induction hypothesis without providing a typing
derivation as second argument.  Formally, the representation of this
derivation must be of type `$\Lof\;({\bf E}\;(\Lfix\; {\bf E}))\;{\bf
T}$'.  Among others, Twelf constructs the term
`$P_1\;(\Lfix\;{\bf E})\;(\Loffix\;P_1)$' which represents the result
of applying the substitution lemma (Lemma~\ref{lem:subst}) as used
in the proof of Theorem~\ref{thm:minitp}.  Recursion then yields the
following subgoal.

\[\begin{array}{l}\AllA{ D_1:\Lev\;({\bf E}\;(\Lfix\;{\bf E}))\;{\bf V},\;
    P_1:\Abs{x}{\Lexp} \Lof\;x\;{\bf T}\arrow \Lof\;({\bf E}\;x)\;{\bf T},\;
    Q_2:\Lof\;{\bf V}\;{\bf T}} \\
  \rspace \ExA{Q_1:\Lof\;{\bf V}\;{\bf T}} \True\end{array}\]

Twelf is now able to determine in a simple filling step that $Q_2$ is a
possible instantiation for $Q_1$, thereby completing the
$\Levfix$-branch of the proof.  The other two branches can be solved
similarly.  Twelf then reports the proof term (currently shown in a more
readable relational notation as an LF signature, rather than in the
functional notation used to define $\Mtwo$).

\subsection {Strategy}

The proof strategy of Twelf is a simple combination of the three
elementary operations.  But each operation must be applied with care
because they are inherently expensive in time and space.  In particular,
we completely avoid backtracking except during the filling step which is
implemented as an iterative deepening depth-first search.  Splitting and
filling (and sometimes also recursion) use unification to analyze cases
and to select constants.  Recursion triggers the calculation of possible
recursion arguments according to the termination ordering
\cite{Rohwedder96esop}.

For a given theorem and induction principle, Twelf attempts to construct
a derivation in $\Mtwo$ using the strategy sketched in
Figure~\ref{fig:strat}.  There is a global store of yet to be proven
subgoals, initialized with the formula representing the theorem.  Once
the automated proof process is started, the strategy {\em activates} a
subgoal and tries to apply a filling operation. 

\begin{figure}[t]
  \begin{center}
    \input{strat.eepic}
  \end{center}
  \caption{Proof strategy}
  \label{fig:strat}
\end{figure}

\subsubsection{Filling:}
The filling operation corresponds to an application of the
$\existsR$-rule: it is applicable, if a substitution instantiating all
existentially quantified variables can be constructed. Because index
variables occur in the types of non-index variables, it is already
enough to determine instantiations for all non-index variables (see
Section~\ref{sec:lf}).  In general, infinitely many substitutions must
be examined, but since our strategy is parametrized by a number to limit
the depth of the search space, the employed search algorithm is
incomplete but will always terminate (even though failure is sometimes
very slow).

If Twelf succeeds in constructing the substitution, the current subgoal
is successfully completed and the next subgoal is selected if available,
otherwise Twelf stops (Q.E.D.).  If Twelf fails to construct the desired
substitution the strategy tries to apply the recursion operation.

\subsubsection{Recursion:}
The recursion operation corresponds to an application of the
$\forallL$-rule, immediately followed by an application of the
$\existsL$-rule: Twelf generates all possible recursive calls by
constructing substitutions which correspond to the arguments of the
recursive call. These substitutions must satisfy the side condition of
the $\fix$-rule.  Because lower-ranked arguments in a lexicographic
termination order actually may increase in size there are potentially
infinitely many different ways to appeal to the induction hypothesis.
Moreover results of inductive calls can be used to form new ones.
Hence, to avoid an infinite chain of applications of induction
hypotheses, our strategy is parameterized by an upper bound of
recursive calls.

If no new recursive calls can be generated, the strategy tries to
apply the splitting operation.

\subsubsection{Splitting:} 
The splitting operation corresponds to an application of the
$\objectL$-rule. It may be applicable if there is at least one
universally quantified variable. Among all those variables, a non-index
variable is selected (see Section~\ref{sec:lf}) whose type is then used
to determine all possible cases ($\sigempty$, $\siguni$, and
$\signonuni$). For each case, a new subgoal is created and one of them
is activated.  Twelf then continues and tries to apply the filling
operation to the newly activated subgoal.

Among all universally quantified variables Twelf selects the one which
generates the least number of subgoals first (which could be zero if a
variable has a dependent type which does not unify with any
constructor type---the subgoal succeeds immediately in that case).  To
avoid that the strategy descends into an infinite loop of splits
(applying splits to the children of a previous split), it is
parametrized by a maximal splitting limit.  This heuristic works
surprisingly well in all of our examples, we leave a refinement of
this heuristic to future research.  If no universally quantified
variables are available, the strategy stops, reporting that the
theorem is not provable with the current filling depth.  It is also
possible that splitting is not applicable because the types of all
universally quantified variables fall outside Miller's pattern
fragment.  In this case Twelf reports that no proof has been found
automatically.

\subsection{Experimental Results}

\begin{figure}[t]
  \begin{center}

\begin{tabular}{|l|r|r|r|r|r|r|}
  \hline         
  {\bf Experiment}&{\bf Ind}&{\bf Lim}&{\bf Filling}&{\bf Splitting}&{\bf Recursion}&{\bf Total}\\
  \hline
  Cartesian Closed Categories&          1&      4&      1.000&  0.004&  0.036&  1.099\\
  \hline
  CPM Completeness&                     1&      20&     0.916&  0.010&  0.117&  1.134\\
  CPM Proof equivalence: $\Arrow$ &     1&      6&      0.226&  0.034&  0.442&  0.951\\
  CPM Proof equivalence: $\Leftarrow$ & 1&      6&      0.280&  0.033&  0.647&  1.235\\
  \hline
  Horn LP Soundness&                    3&      4&      4.336&  0.004&  0.049&  4.501\\
  Horn LP Canonical forms&              3&      4&      0.028&  0.009&  0.107&  0.303\\
  Horn LP Completeness&                 2&      4&      0.015&  0.005&  0.039&  0.195\\
  \hline
  Mini-ML Value soundness &             1&      3&      0.016&  0.041&  0.061&  0.172\\
  Mini-ML Type preservation&            1&      6&      0.062&  0.521&  0.150&  0.799\\
  Mini-ML Evaluation/Reduction&         1&      9&      25.397& 0.007&  0.078&  25.546\\
  \hline
  Hilbert's abstraction theorem&        1&      4&      0.197&  0.004&  0.010&  0.322\\
  \hline
  Associativity of $+$&                 1&      3&      0.009&  0.012&  0.016&  0.063\\
  Commutativity of $+$&                 2&      3&      0.092&  0.609&  4.139&  4.877  \\
\hline
\end{tabular}

%    \begin{tabular}{|l|r|r|r|r|r|r|}
%      \hline
%      Experiment & Induction & Limit  & Recursive & \multicolumn{2}{c|}{Lines} &Time \\[-1ex]
%      &           &        & Calls     & (no imp) & (imp) & \\
%      \hline
%      Value Soundness             & 1 & 6  & 11 & 23 & 50 &0.3 sec \\
%      Type Preservation           & 1 & 6  & 15 & 35 & 106 &1.9 sec \\
%      Completeness: Semantics      & 1 & 20 & 16 & 100 & 316 &8.3 sec \\
%      Proof equivalence: Completeness  & 1 & 6  & 16 & 29 & 484 &17.7 sec\\
%      Proof equivalence: Soundness  & 1 & 6  & 16 & 29 & 506 &17.1 sec\\
%      \hline
%      Deduction Theorem           & 1 & 6  & 2 & 7 & 26 &1.6 sec \\
%      Completeness: Logic Pogramming & 3 & 4  & 8 & 20 & 41 &0.5 sec \\
%      Cartesian Closed Categories & 1 & 6  & 5 & 15 & 32 &120.2 sec \\
%      \hline
%    \end{tabular}
  \end{center}
  \caption{Experimental results}
  \label{fig:exp}
\end{figure}
Twelf has been successfully employed to prove several non-trivial
theorems automatically. In Figure~\ref{fig:exp} we give an overview
over the experimental results from the areas of programming languages
and logics. ``Ind'' states how many theorems have been simultaneously
proven and ``Lim'' the maximal search depth for LF objects. In all
examples the maximal splitting limit is $2$, and the number of recursive
calls is limited to $10$ for each subgoal.  Besides
the time for ``Filling'', ``Splitting'', and ``Recursion'', 
``Total'' also summarizes time spent for parsing, and type reconstruction.
%The left column of the ``line''
%counter shows the length of the proof when implicit arguments are
%suppressed, the right column the natural length. 
All timings have been
taken on a 300 Mhz Pentium-II machine, running Linux 2.30, New Jersey
SML 110, and Twelf 1.2.
 
In the area of Mini-ML Twelf was used to prove value soundness, i.e.\ 
that if $\ev{e}{v}$ then $v$ is a value, and type preservation
(Theorem~\ref{thm:minitp}).  Moreover, it was used to show the
completeness of a continuation stack machine with respect to a natural
semantics for Mini-ML. In the proof, Twelf constructed a mapping from
Mini-ML evaluation derivations to computation traces of the abstract
machine. But it could not verify the soundness direction, because the
proof requires complete induction which is not supported by the
current implementation. Nonetheless, Twelf could prove that the
soundness proof (coded by hand) always resembles the completeness
proof in structure. For this proof, it constructed a function mapping
soundness proofs into completeness proofs and vice versa.

In the area of logic, Twelf was used to derive, among others, the
proof of the deduction theorem for intuitionistic propositional logic
using Hilbert's axiomatization which is used to translate pure
functional programs into combinators. It also proved soundness and
completeness of uniform derivations with respect to resolution for
Horn-logic. From the area of category theory, it proved that
Cartesian closed categories can be embedded into the simply-typed
$\lambda$-calculus.  

\section{Related Work and Future Work} \label{sec:rel}

There have been many mechanized proofs of meta-theoretic properties of
logics or programming languages in the literature (see the
survey~\cite{Pfenning96caap}).  Most of these do not use techniques
from logical frameworks, but represent the languages via standard
inductive types and their semantics by inductively defined predicates.
A popular choice for such encodings are de Bruijn indices, since they
eliminate the problem of $\alpha$-conversion from consideration.
However, various lemmas regarding substitution must still be shown and
used, which severely limits the degree of automation which can be
achieved.  Most closely related to our own efforts in this area is the
work on ALF~\cite{Magnusson95}, since ALF also employs dependently
typed pattern matching and termination orderings, although without the
benefits of higher-order abstract syntax, but with a simpler notion of
proof by induction.

At the opposite extreme we have work on representing meta-theoretic
proofs as relations in LF, which leaves the progress and termination
properties above to an external check on relations (only type
soundness is directly guaranteed by type-checking in
LF)~\cite{Pfenning92cade}.  In this approach, we have no automation
besides type reconstruction.  The expressive power of LF makes this
feasible, but it remains tedious.

Most closely related to our approach is work by McDowell and
Miller~\cite{McDowell97lics} who also define a higher-order meta-logic
$\foldn$ for a logical framework (hereditary Harrop formulas) and then
reason in the meta-logic.  Their approach is based entirely on simple
types and does not incorporate proof terms, which makes it less
suitable for automation.  Moreover, in order to establish consistency
for their meta-logic, they limit induction to natural numbers, which
also complicates automation.  In fact, their implementation based on
the Pi proof editor~\cite{Eriksson94cade} is entirely interactive.  On
the other hand, McDowell has demonstrated the flexibility of his
approach in his thesis~\cite{McDowell97phd} where he also treats a
logical framework which incorporates linearity.  Since the overall
architecture is quite similar, this gives us confidence that our
approach may be extended to a linear logical
framework~\cite{Cervesato96lics}, which is planned in future work.  We
believe that the separation between logical framework and meta-logic,
and the separation between definition by cases and well-founded
recursion are all critical ingredients in making this idea successful
for even richer logical frameworks than LF\@.

While the set of theorems we can prove at present is already
surprisingly rich, they are limited by three factors: (1) we do not
attempt to automatically use lemmas, (2) only lexicographic extensions
of subterm orderings are permitted to show termination, and (3) $\Mtwo$
does not support reasoning about \emph{open} LF objects.  We believe
that (1) and (2) can be addressed by incorporating standard techniques
from inductive theorem proving, efficiency improvements such as
indexing, and simply allowing more complex termination orderings.
Nonetheless, we have currently no plans for developing Twelf into a
general-purpose theorem prover, because we feel that its present success
owes mostly to its design as a special-purpose prover for properties of
programming languages and logics.  We are currently investigating how to
incorporate ideas from schema-checking~\cite{Rohwedder94proposal} and primitive
recursion over higher-order abstract syntax~\cite{Despeyroux97} into
our meta-logical framework in order to make progress on item (3), that
is, allow reasoning over terms which may have free variables from
certain ``regular'' contexts which arises in many practical examples.

%-----------------------------------------------------------------------

\bibliography{/afs/cs/usr/carsten/bib/all,/afs/cs/usr/carsten/bib/lfs,/afs/cs/usr/carsten/bib/coq,/afs/cs/usr/carsten/bib/martinloef,/afs/cs/usr/carsten/bib/linear,/afs/cs/usr/carsten/bib/pvs,/afs/cs/usr/carsten/bib/isabelle,cade98}
\appendix
\end{document}



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 




