paper.tex

\documentclass[submission,copyright,creativecommons]{eptcs}
\providecommand{\event}{ACL2 Workshop 2017} % Name of the event you are submitting to
% \usepackage{breakurl}             % Not needed if you use pdflatex only.
\usepackage{amsmath,amssymb,amsfonts,amsthm}
\usepackage{fancyvrb}
% so we can use \-/ for breakable dashes in long names
\usepackage[shortcuts]{extdash}
% \usepackage{bigfoot}
% \usepackage{tikz}
\usepackage{color}
\usepackage{framed}

% \newtheorem{theorem}{Theorem}
% \newtheorem{corollary}{Corollary}

% The first of the following two definitions of the comment
% environment is adapted from
% http://tex.stackexchange.com/questions/71371/how-to-change-color-in-an-environment
% while the second comes from a package.  Choose the first to see
% comments and the second to hide them.

\newenvironment{comment}
  {\par\medskip
   \color{red}%
   \begin{framed}
   \ignorespaces}
 {\end{framed}
  \medskip}

% \usepackage{comment}

% Neither of the following worked for me:

%\newenvironment{mycomment}{{\begin{comment}}}{{\end{comment}}}

% \let\mycomment\comment
% \let\endmycomment\endcomment

\usepackage{listings}
\lstset{ %
  basicstyle=\normalsize\ttfamily,
  language=lisp,
  columns=fullflexible,
  escapeinside={\<}{\>},
}

\newcommand*{\var}[1]{\mathit{#1}}

% The following comment is from Reviewer 3:
%%% The title is short-and-sweet, but perhaps too short.  It would be
%%% nice if the title conveyed more information to the ACL2-curious
%%% user of other theorem provers; something like "Using Meta-extract
%%% to Craft Custom Proof Routines in ACL2" (using language from the
%%% paper).
% I don't like the suggested new title, because it might suggest that
% this paper is about the addition of meta rules.  I was tempted to
% make the title "Meta-extract: Reflecting What We Know", but that's
% too obscure.  Maybe: "Meta-extract: Bringing Implicit Knowledge to
% Bear".  I dunno.  Ideas?

\title{Meta-extract: Using Existing Facts in Meta-reasoning}
\author{Matt Kaufmann
\institute{Department of Computer Science\\
The University of Texas at Austin\\
Austin, TX, USA}
\email{kaufmann@cs.utexas.edu}
\and
Sol Swords
\institute{Centaur Techology, Inc.\\
Austin, TX, USA}
\email{sswords@centtech.com}
}
\def\titlerunning{Meta-extract}
\def\authorrunning{M. Kaufmann \& S. Swords}
\begin{document}
\maketitle

\begin{abstract}

  ACL2 has long supported user-defined simplifiers, so-called {\em
    metafunctions} and {\em clause processors}, which are installed
  when corresponding rules of class {\tt :meta} or {\tt
    :clause-processor} are proved.  Historically, such
  simplifiers could access the logical world at execution time and
  could call certain built-in proof tools, but one could not assume the
  soundness of the proof tools or the truth of any facts extracted
  from the world or context when proving a simplifier correct.  Starting with
  ACL2 Version 6.0, released in December 2012, an additional
  capability was added which allows the correctness proofs of
  simplifiers to assume the correctness of some such proof tools and
  extracted facts.  In this paper we explain this capability and give
  examples that demonstrate its utility.

\end{abstract}

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

\section{Meta-extract}
\label{sec:meta-extract}
\input{meta-extract}

\section{Using ``meta-extract-user.lisp''}
\label{sec:user}
\input{wrapper}

\section{Applications}
\label{sec:applications}
\input{applications}

% No related work section; see top of related.tex
% \section{Related Work}
% \label{sec:related}
% \input{related}

\section{Conclusion}
\label{sec:conclusion}
\input{conclusion}

\section*{Acknowledgments}

% Matt had some chats with J about this stuff back in 2012.
We thank J Moore for helpful discussions.
We also thank the referees for useful feedback.
This material is based upon work supported in part by DARPA under
Contract No. FA8750-15-C-0007 (subcontract 15-C-0007-UT-Austin)
and by ForrestHunt, Inc.

% \nocite{*}
\bibliographystyle{eptcs}
\bibliography{paper}
\end{document}