[Hol-checkins] CVS: hol98/examples/dev/doc/tphols2005 gtkwave.epsi,NONE,1.1 paper.tex,NONE,1.1

[Mike G. <mj...@us...>]

Update of /cvsroot/hol/hol98/examples/dev/doc/tphols2005
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv32648

Added Files:
	gtkwave.epsi paper.tex 
Log Message:
A new version of the TPHOLs submission paper that incorporates a dump
from gtkwave showing the HOL synthesised Verilog computing factorial 8. 
Have also folded all the files into a single document: paper.tex.



--- NEW FILE: gtkwave.epsi ---
%!PS-Adobe-2.0 EPSF-1.2
%%Title: gtkwave.ps
%%Creator: Ghostscript ps2epsi from gtkwave.ps
%%CreationDate: Mar 30 12:54
%%For:mjcg mjcg
%%Pages: 1
%%DocumentFonts: Courier
%%BoundingBox: 31 539 179 792
%%BeginPreview: 148 253 8 1012
% 21000000000000000000000000000000000000000000000000000000000000000000000000000000
% 00000000000000000000000000000000000000000000000000000000000000000000000000000000
% 00000000000000000000000000000000000000000000000000000000000000000000210000000000
% 00000000000000000000000000000000000000000000000000000021
% 21000000000000000000000000000000000000000000000000000000000000000000000000000000
% 00000000000000000000000000000000000000000000000000000000000000000000000000000000
% 00000000000000000000000000000000000000000000000000000000000000000000210000000000
% 00000000000000000000000000000000000000000000000000000021
% 21000000000000000000000000000000000000000000000000000000000000000000000000000000
% 00000000000000000000000000000000000000000000000000000000000000000000000000000000
[...2260 lines suppressed...]
313 104 313 92 l
0 1 0 rgb
313 104 338 104 l
0 1 0 rgb
313 92 338 92 l
0 1 0 rgb
315 102 (20+) s
0 1 0 rgb
338 104 338 92 l
0 1 0 rgb
338 104 463 104 l
0 1 0 rgb
338 92 463 92 l
0 1 0 rgb
340 102 (40320) s
grestore showpage
%%EndDocument
%%Trailer
cleartomark countdictstack exch sub { end } repeat restore
%%EOF

--- NEW FILE: paper.tex ---
\documentclass{llncs}
\usepackage{epic,eepic,subfigure,alltt,graphicx}
\input{notation.tex}

%--------------------------------------------------------------------------
\title{A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic}

\author{}
\institute{}

\begin{document}
\maketitle

\vspace*{-8mm}

\begin{center}
\begin{tabular}{ccc}
{\bf Mike Gordon, Juliano Iyoda} &\hspace*{5mm}& {\bf Scott Owens, Konrad Slind}\\
University of Cambridge          &\hspace*{5mm}& University of Utah\\
[...1250 lines suppressed...]
         \label{figAtom}\input{atm.eepic}\hspace*{0cm}}
      \subfigure[$\DEF{SEQ}\ f\ g$]{
         \label{figSeq}\input{seq.eepic}\hspace*{0cm}}
      \subfigure[$\DEF{PAR}\ f\ g$]{
         \label{figPar}\input{par.eepic}}}
      \caption{\label{figSeqPar}Implementation of composite devices.}
\end{figure}
\begin{figure}[htb]
   \centerline{
       \subfigure[$\DEF{IF}\ e\ f\ g$]{
           \label{figIf}\input{ifReduced.eepic}\hspace*{0.3cm}}
       \subfigure[$\DEF{REC}\ e\ f\ g$]{
           \label{figRec}\input{recReduced.eepic}\hspace*{0cm}}}
   \caption{\label{figIfRec}The conditional and the recursive constructors.}
\end{figure}

\end{document}
% LocalWords:  langle