%-------------------------------------------------------------------------------
% Topmatter                                                                     
%-------------------------------------------------------------------------------

\documentclass[11pt,twoside]{article}
\usepackage{noweb,fullpage,clrscode,proof,hyperref,amsmath,amssymb}
\usepackage[open-square,define-standard-theorems,roman-theorems]{QED}

%-------------------------------------------------------------------------------
% Title                                                                         
%-------------------------------------------------------------------------------

\title{Towards a Focusing Inverse-Method Theorem Prover for Canonical LF}
\author{Sean McLaughlin}

%-------------------------------------------------------------------------------
% Begin                                                                         
%-------------------------------------------------------------------------------

\begin{document} 
\maketitle
\arraycolsep=12pt
\input{commands.tex}

%-------------------------------------------------------------------------------
% Abstract                                                                      
%-------------------------------------------------------------------------------

\begin{abstract} 
This is an experiment at implementing \emph{Canonical LF}.  We intend
to present muliple forms of representation.  We will begin with a
simple name-carrying implementation of Canonical LF.  We will continue
with spine forms and explicit substitutions, and finally add
meta-variables.  Through this process, we hope to experiment with the
various representations to find a good trade-off between efficiency
and elegance.
\end{abstract} 

%-------------------------------------------------------------------------------
% Canonical LF                                                                  
%-------------------------------------------------------------------------------

\input{canonical.tex}

%-------------------------------------------------------------------------------
% Typechecking                                                                  
%-------------------------------------------------------------------------------

While we have just described Canonical LF, a language where all
expressions are canonical, it is sometimes useful to relax the canonicity
restriction to take advantage of various implementation 
techniques.  To get a better idea of the efficiency of various
implementations, we present here two different methods of
typechecking, called \emph{eager} and \emph{lazy}, with
two minor variants of each method.

\input{eagercheck.tex}
\input{lazycheck.tex}

%-------------------------------------------------------------------------------
% The Inverse Method                                                            
%-------------------------------------------------------------------------------

\input{inverse.tex}

%-------------------------------------------------------------------------------
% Appendices                                                                    
%-------------------------------------------------------------------------------

%% \input{twelf_grammar.tex}
%% \input{using.tex}

%-------------------------------------------------------------------------------
% Bibliography                                                                  
%-------------------------------------------------------------------------------

\bibliographystyle{abbrv}
\bibliography{all}

%-------------------------------------------------------------------------------
% End                                                                           
%-------------------------------------------------------------------------------

\end{document}
