\documentstyle{article}
\oddsidemargin 0in
\evensidemargin 0in
\topmargin 0in
\textheight 9in
\textwidth 6.5in
\setlength{\topmargin}{-0.5in}
\parindent 0in
\raggedbottom
\newcommand{\f}[1]{{\tt #1}}

\title{Classified Larch Bibliography}
\author{Stephen J. Garland}
\date{October 22, 1996}

\begin{document}
\bibliographystyle{plain}
%\bibliographystule{abbrv}

\maketitle

This classified bibliography is an updated version of Appendix C in
\cite{Guttag93}.  Papers of historical interest only are included among the
references, but do not appear in the classification.

The \LaTeX files used to prepared this bibliography are available over the WWW
from the Larch home page, \f{http://larch.lcs.mit.edu:8001/larch/index.html}.
\f{ftp} from Internet node \f{larch.lcs.mit.edu} as
Please send corrections and suggested additions to \f{larch@lcs.mit.edu}.
Kindly include a brief description of each suggested addition so that it can be
cited in appropriate categories.


\section*{Papers about Larch}

\subsection*{Current work}

An overview of Larch is available in \cite{Guttag93}, which describes the Larch
Shared Language and the Larch/C interface language.  It also provides an
introduction to the Larch Prover and the Larch/Modula-3 interface language.

Reports about the current status of several Larch-related projects are
contained in \cite{Martin92}.

\subsection*{Larch languages}

\nocite{Guttag85,Guttag85a}

Larch Shared Language: \cite{Guttag93,Horning95}
\nocite{Guttag86,Guttag86a,Guttag86b,Guttag90}

Larch Interface Languages
\begin{itemize}
\item Generic \cite{Chen89,Hinman87,Lerner91,Wing87a}
\item Ada \cite{Guaspari90}
\item C \cite{Feldman92,Guttag93,Tan92,Tan94a,Tan94b,Tan95}
        \nocite{Guttag91,Guttag91a}
\item C++ \cite{Leavens92}
\item CLU \cite{Wing83}
\item ML \cite{Wing92}
\item Modula-3 \cite{Jones92,Jones91,Jones92a,Guttag93}
\item Smalltalk \cite{Cheon91}
\end{itemize}

Larch and other methods: \cite{Baugh92a,Guttag93,Guttag93a,Liskov86,Wing91a}
\nocite{Garland93,Guttag74,Guttag75,Guttag79,Guttag78a,Horning85}

\subsection*{Larch tools}

LP, the Larch Proof Assistant
\begin{itemize}
\item User's Guide: \cite{Garland91,Garland95}
\item Distributed LP (DLP): \cite{Vandevoorde96}
\item Beginner's strategy guide: \cite{Taylor90}
\item Extensions: \cite{Vogt90}
\item Use: \cite{Bidoit92,Broy92,Buth92,Chetali92,Choppy92,Scott92,Voisin92}
\end{itemize}
\nocite{Garland88a,Garland89}

For LSL: \cite{Bourdeau92,Laux92}

For LCL: \cite{Evans94a,Evans94b,Evans96,Feldman92}

For LM3: \cite{Jones92}

\section*{Sample specifications}

Apple MAC Toolbox: \cite{Burton89}

Avalon built-in classes, examples (queue, directory, counter):
\cite{Lerner91,Wing89a,Wing88,Wing90a}
\nocite{Wing90}

Database: \cite{Guttag93}

Display: \cite{Guttag80}

Distributed algorithms: \cite{Luchangco94,Petrov96,Sogaard93}

Finite element analysis library: \cite{Baugh92,Baugh89}

Garbage collection: \cite{Detlefs90}

IOStreams: \cite{Jones91}

Larch/Ada: \cite{Cardenas88,Guaspari90}

Library: \cite{Wing87}

Miro languages and editor: \cite{Wing91,Zaremski91}

Thread synchronization primitives: \cite{Birrell87,Nelson91}

Using specifications to search software libraries: \cite{Rollins91}

\section*{Proofs using LP}

Ada programs: \cite{Guaspari92}

Analysis of Larch specifications: \cite{Guttag93}
\nocite{Garland90b,Garland90c}

Avalon queue example: \cite{Gong89,Wing89,Wing90a}

Circuit examples: 
\cite{Chetali92,Garland88c,Mellergaard92,Saxe93,Staunstrup89,Staunstrup92}
\nocite{Saxe92}

Compiler optimizations: 
\cite{Vandevoorde92,Vandevoorde93,Vandevoorde94a,Vandevoorde94b}.

Distributed algorithms: \cite{Luchangco94,Petrov96,Sogaard93}

Mathematical Theorems: \cite{Martin90}
\nocite{Lescanne83}

Temporal Logic of Actions: \cite{Engberg92}


\bibliography{larch}
\end{document}

