--- a/Paper/Paper.thy Wed Mar 17 20:42:42 2010 +0100
+++ b/Paper/Paper.thy Thu Mar 18 00:17:21 2010 +0100
@@ -2,6 +2,13 @@
theory Paper
imports "../Nominal/Test"
begin
+
+notation (latex output)
+ swap ("'(_ _')" [1000, 1000] 1000) and
+ fresh ("_ # _" [51, 51] 50) and
+ supp ("supp _" [78] 73) and
+ uminus ("-_" [78] 73) and
+ If ("if _ then _ else _" 10)
(*>*)
section {* Introduction *}
@@ -22,16 +29,69 @@
involving general bindings are alpha-equivelent.
*}
-section {* A Brief Overview about the Nominal Logic Work *}
+section {* A Short Review of the Nominal Logic Work *}
+
+text {*
+ At its core, Nominal Isabelle is based on the nominal logic work by Pitts
+ \cite{Pitts03}. The central notions in this work are sorted atoms and
+ permutations of atoms. The sorted atoms represent different
+ kinds of variables, such as term- and type-variables in Core-Haskell, and it
+ is assumed that there is an infinite supply of atoms for each sort.
+ However, in order to simplify the description of our work, we shall
+ assume in this paper that there is only a single sort of atoms.
+
+ Permutations are bijective functions from atoms to atoms that are
+ the identity everywhere except on a finite number of atoms. There is a
+ two-place permutation operation written
+
+ @{text [display,indent=5] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+
+ \noindent
+ with a generic type in which @{text "\<alpha>"} stands for the type of atoms
+ and @{text "\<beta>"} for the type of the objects on which the permutation
+ acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"},
+ the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}
+ and the inverse permutation @{term p} as @{text "- p"}. The permutation
+ operation is defined for products, lists, sets, functions, booleans etc
+ (see \cite{HuffmanUrban10}).
+
+ The most original aspect of the nominal logic work of Pitts et al is a general
+ definition for ``the set of free variables of an object @{text "x"}''. This
+ definition is general in the sense that it applies not only to lambda-terms,
+ but also to lists, products, sets and even functions. The definition depends
+ only on the permutation operation and on the notion of equality defined for
+ the type of @{text x}, namely:
+
+ @{thm [display,indent=5] supp_def[no_vars, THEN eq_reflection]}
+
+ \noindent
+ There is also the derived notion for when an atom @{text a} is \emph{fresh}
+ for an @{text x}, defined as
+
+ @{thm [display,indent=5] fresh_def[no_vars]}
+
+ \noindent
+ A striking consequence of these definitions is that we can prove
+ without knowing anything about the structure of @{term x} that
+ swapping two fresh atoms, say @{text a} and @{text b}, leave
+ @{text x} unchanged. For the proof we use the following lemma
+ about swappings applied to an @{text x}:
+
+*}
+
section {* Abstractions *}
section {* Alpha-Equivalence and Free Variables *}
+section {* Examples *}
+section {* Conclusion *}
text {*
- Acknowledgements: We thank Andrew Pitts for the many discussions
+
+ \noindent
+ {\bf Acknowledgements:} We thank Andrew Pitts for the many discussions
about the topic. We thank Peter Sewell for making [] available
to us and explaining some of the finer points of the OTT tool.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/acmconf.cls Thu Mar 18 00:17:21 2010 +0100
@@ -0,0 +1,442 @@
+% ACMCONF DOCUMENT CLASS
+% adapted from ARTICLE document style by Ken Traub
+% Hacked for [preprint] option by Olin Shivers 4/91
+% Fixed up for LaTeX version 2e [compatibility mode] by Peter Lee 10/9
+% (with help from Simon Peyton Jones)
+% Converted to a LaTeX2e document class by David A. Berson 11/94
+%
+% ARTICLE DOCUMENT STYLE -- Released 16 March 1988
+% for LaTeX version 2.09
+% Copyright (C) 1988 by Leslie Lamport
+
+% To do:
+% - Possibly move the commands related to 9pt size to a file size9.clo
+% and write the stuff to unpack both acmconf.cls and size9.clo files
+% from a single distribution file.
+
+%%% ACMCONF is a document class for producing two-column camera-ready pages for
+%%% ACM conferences, according to ACM specifications. The main features of
+%%% this class are:
+%%%
+%%% 1) Two columns.
+%%% 2) Side and top margins of 4.5pc, bottom margin of 7.5pc, column gutter of
+%%% 2pc, hence columns are 20pc wide and 54pc tall. (6pc = 1in, approx)
+%%% 3) First page has title information, and an extra 4.5pc of space at the
+%%% bottom of the first column for the ACM copyright notice. (You must
+%%% use one of the commands \copyrightspace or \toappear{} to obtain this
+%%% space.)
+%%% 4) Text is 9pt on 10pt baselines; titles are 9pt bold sans-serif.
+%%% (The acmconf.sty from which acmconf.cls was derived actually uses
+%%% 9pt bold roman for section titles. Functionally, I have left this
+%%% as is. I have added a commented out alternate defination of
+%%% \acmtitlestyle that uses sans-serif) --DAB
+%%%
+%%% This document class supports a [preprint] class option that allows you
+%%% to run off a copy for a preprint -- with page numbers, "to appear"
+%%% information, and so forth. This is documented below.
+
+%%% There are a few restrictions you must observe:
+%%%
+%%% 1) You cannot change the font size; ACM wants you to use 9pt.
+%%% 3) You must start your paper with the \maketitle command. Prior to the
+%%% \maketitle you must have \title and \author commands. If you have a
+%%% \date command it will be ignored; no date appears on the paper, since
+%%% the proceedings will have a date on the front cover.
+%%% Optionally, you may have an \affiliation command with text, such
+%%% as company or university name and address, that will be centered
+%%% just below the author(s).
+%%% 4) Marginal paragraphs, tables of contents, lists of figures and tables,
+%%% and page headings are all forbidden.
+%%% 5) The `figure' environment will produce a figure one column wide; if you
+%%% want one that is two columns wide, use `figure*'. Ditto for the
+%%% `table' and `table*' environments.
+%%%
+%%% Page Headings:
+%%% Normally, \pagestyle commands are ignored --- pages have no headings or
+%%% numbers. ACM will number the pages for you when they are inserted into the
+%%% proceedings (you should put page numbers on the BACK of each page, though,
+%%% in case someone drops your paper on the floor).
+%%%
+%%% If the [preprint] option is present, then \pagestyle commands are obeyed,
+%%% and the default is \pagestyle{plain}. The [twoside] option is also
+%%% useful when using headers.
+%%%
+%%% The [draft] and [final] options as used in the article class are also
+%%% supported.
+%%%
+%%%
+%%% Copyright Space:
+%%% You leave space at the bottom of page 1/column 1 one with the
+%%% \copyrightspace command. Alternatively, you can use the
+%%% \toappear{...} command. Normally, this turns into an unnumbered
+%%% footnote 4.5pc high. If [preprint] is on, then this space is
+%%% filled with the {...} text; otherwise, it's blank. You must put
+%%% one of these commands in the text of page 1/column 1 *after* all the
+%%% other footnotes that go on page1/column 1, of course.
+%%%
+%%% A typical usage looks like this:
+%%% \toappear{To appear in the Ninth AES Conference on Midevil Lithuanian
+%%% Embalming Technique, June 1991, Alfaretta, Georgia.
+%%% Also available as Technical Report CMU-CS-91-119,
+%%% Cranberry Melon School of Cucumber Science.}
+%%% This will be included in the preprint, and left out of the conference
+%%% version.
+%%%
+%%% Acmconf defines two useful conditionals.
+%%% - \ifacmconf{true-stuff}{false-stuff}
+%%% expands to true-stuff.
+%%% - \ifpreprint true-stuff \else else-stuff \fi
+%%% expands to true-stuff if the [preprint] option is being used,
+%%% otherwise it expands to else-stuff.
+%%% \ifacmconf is a latex command; \ifpreprint is a real latex conditional.
+%%%
+%%% WARNING:
+%%% Some dvi-ps converters heuristically allow chars to drift from their
+%%% true positions a few pixels. This loses noticeably with the 9pt sans-serif
+%%% bold font used for section headers. You turn this hackery off in our
+%%% dvi-ps converters with the -e option:
+%%% dvips -e 0 foo.dvi >foo.ps
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesClass{acmconf}[1994/11/27 Alternative LaTeX document class]
+\typeout{Bugs to berson@cs.pitt.edu}
+
+%
+% Define the conditionals and command for the options.
+%
+\newif\if@acmconf\@acmconftrue
+\long\def\ifacmconf#1#2{\if@acmconf#1\else#2\fi}
+\newif\ifpreprint
+
+%
+% Declare and process the options
+%
+\DeclareOption{draft}{\PassOptionsToClass{draft}{article}}
+\DeclareOption{final}{\PassOptionsToClass{final}{article}}
+\DeclareOption{twocolumn}{\PassOptionsToClass{twocolumn}{article}}
+\DeclareOption{twoside}{\PassOptionsToClass{twoside}{article}}
+\DeclareOption{preprint}{\preprintfalse}
+%\DeclareOption{preprint}{\preprinttrue}
+%
+% Let them off with just a warning for any other option
+%
+\DeclareOption*{\ClassWarningNoLine{acmconf}{Unknown option `\CurrentOption'}}
+%\DeclareOption*{\ClassError{acmconf}
+% {The `\CurrentOption' option is not supported}
+% {Remove the `\CurrentOption' option from the
+% \protect\documentclass\space line.}}
+
+\ExecuteOptions{twocolumn}
+\ProcessOptions
+
+%
+% This class simply modifies a few behaviors of the article class,
+% so load it now
+%
+\LoadClass{article}
+
+
+%**********************************************************************
+%
+% The following commands would normally be in a file such as
+% size9.clo for the article class. Since the size isn't really an
+% option, I include them here. I have followed the order of the commands
+% as found in size10.clo.
+%
+% I could test for the presence of % the file size9.clo and load it when
+% availale, instead of executing these commands.
+%
+
+%
+% Set the font sizes and spacing
+%
+\renewcommand\baselinestretch{1}
+
+\renewcommand\normalsize{%
+ \@setfontsize\normalsize\@ixpt\@xpt
+ \abovedisplayskip 9\p@ \@plus2\p@ \@minus4.5\p@%
+ \abovedisplayshortskip \z@ \@plus3\p@%
+ \belowdisplayshortskip 5.4\p@ \@plus3\p@ \@minus3\p@%
+ \belowdisplayskip \abovedisplayskip
+ \let\@listi\@listI}
+\normalsize
+\renewcommand\small{%
+ \@setfontsize\small\@viiipt{9}%
+ \abovedisplayskip 7.6\p@ \@plus 3\p@ \@minus 4\p@%
+ \abovedisplayshortskip \z@ \@plus2\p@%
+ \belowdisplayshortskip 3.6\p@ \@plus2\p@ \@minus 2\p@
+ \def\@listi{\leftmargin\leftmargini
+ \topsep 4\p@ \@plus 2\p@ \@minus 2\p@
+ \parsep 2\p@ \@plus 1\p@ \@minus 1\p@
+ \itemsep \parsep}
+ \belowdisplayskip \abovedisplayskip
+}
+\renewcommand\footnotesize{%
+ \@setfontsize\footnotesize\@viipt{8}
+ \abovedisplayskip 6.4\p@ \@plus 2\p@ \@minus 4\p@%
+ \abovedisplayshortskip \z@ \@plus 1\p@%
+ \belowdisplayshortskip 2.7\p@ \@plus 1\p@ \@minus 2\p@
+ \def\@listi{\leftmargin\leftmargini
+ \topsep 3\p@ \@plus 1\p@ \@minus 1\p@
+ \parsep 2\p@ \@plus 1\p@ \@minus 1\p@
+ \itemsep \parsep}%
+ \belowdisplayskip \abovedisplayskip
+}
+\renewcommand\scriptsize{\@setfontsize\scriptsize\@viipt{8pt}}
+\renewcommand\tiny{\@setfontsize\tiny\@vpt{6pt}}
+\renewcommand\large{\@setfontsize\large\@xipt{13.6\p@}}
+\renewcommand\Large{\@setfontsize\Large\@xiipt{14\p@}}
+\renewcommand\LARGE{\@setfontsize\LARGE\@xivpt{18\p@}}
+\renewcommand\huge{\@setfontsize\huge\@xviipt{22\p@}}
+\renewcommand\Huge{\@setfontsize\Huge\@xxpt{25\p@}}
+
+\setlength\parindent{13.5\p@} % This is what normally used for one
+ % column. Should it be 1em for us?
+\setlength\headheight{0\p@}
+\setlength\headsep{0\p@}
+\setlength\headheight{0\p@}
+\setlength\headsep{0\p@}
+\setlength\footskip{30\p@}
+%
+% There was no \topskip or \@maxdepth in the original acmconf.sty.
+% Thus, we inherit
+%\topskip 10pt
+%\maxdepth .5\topskip
+% from size10.clo loaded via article.cls
+%
+\setlength\textwidth{42pc}
+\setlength\textheight{650\p@}
+\setlength\oddsidemargin{4.5pc}
+\addtolength\oddsidemargin{-1in} % Correct for LaTeX gratuittousness
+\setlength\evensidemargin{4.5pc}
+\addtolength\evensidemargin{-1in} % Correct for LaTeX gratuittousness
+\setlength\marginparwidth{0\p@} % Margin pars are not allowed.
+\setlength\marginparsep{11\p@}
+\setlength\marginparpush{5\p@}
+\setlength\topmargin{4.5pc}
+\addtolength\topmargin{-1in} % Correct for LaTeX gratuitousness
+%
+% I wonder if these next three lines should only be executed if
+% the preprint option is in effect? -- DAB
+%
+%% Must redefine the top margin so there's room for headers and
+%% page numbers if you are using the preprint option. Footers
+%% are OK as is. Olin.
+\addtolength\topmargin{-37\p@} % Leave 37pt above text for headers
+\setlength\headheight{12\p@}
+\setlength\headsep{25\p@}
+
+\setlength\footnotesep{5.6\p@}
+\setlength{\skip\footins}{8.1\p@ \@plus 4\p@ \@minus 2\p@}
+\setlength\floatsep{11\p@ \@plus 2\p@ \@minus 2\p@}
+\setlength\textfloatsep{18\p@ \@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep{11\p@ \@plus 2\p@ \@minus 2\p@}
+\setlength\dblfloatsep{11\p@ \@plus 2\p@ \@minus 2\p@}
+\setlength\dbltextfloatsep{18\p@ \@plus 2\p@ \@minus 4\p@}
+%
+% These values will be inherited from the default size10.clo file
+% included when we load the base article class. I include them
+% here for completeness in case we split out the size9.clo file someday.
+% --DAB
+\setlength\@fptop{0\p@ \@plus 1fil}
+\setlength\@fpsep{8\p@ \@plus 2fil}
+\setlength\@fpbot{0\p@ \@plus 1fil}
+\setlength\@dblfptop{0\p@ \@plus 1fil}
+\setlength\@dblfpsep{8\p@ \@plus 2fil}
+\setlength\@dblfpbot{0\p@ \@plus 1fil}
+\setlength\partopsep{2\p@ \@plus 1\p@ \@minus 1\p@}
+%
+% I think that all of these should be renewcommands. I also think
+% that \setlength should be used. But, they are not in the size10.clo
+% file that I am following. --DAB
+%
+\renewcommand\@listI{\leftmargin\leftmargini
+ \parsep 3.6\p@ \@plus 2\p@ \@minus 1\p@%
+ \topsep 7.2\p@ \@plus 2\p@ \@minus 4\p@%
+ \itemsep 3.6\p@ \@plus 2\p@ \@minus 1\p@}
+\let\@listi\@listI
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+ \labelwidth\leftmarginii
+ \advance\labelwidth-\labelsep
+ \topsep 3.6\p@ \@plus 2\p@ \@minus 1\p@
+ \parsep 1.8\p@ \@plus 0.9\p@ \@minus 0.9\p@
+ \itemsep \parsep}
+\def\@listiii{\leftmargin\leftmarginiii
+ \labelwidth\leftmarginiii
+ \advance\labelwidth-\labelsep
+ \topsep 1.8\p@ plus 0.9\p@ minus 0.9\p@
+ \parsep \z@
+ \partopsep 1\p@ plus 0\p@ minus 1\p@
+ \itemsep \topsep}
+\def\@listiv {\leftmargin\leftmarginiv
+ \labelwidth\leftmarginiv
+ \advance\labelwidth-\labelsep}
+\def\@listv {\leftmargin\leftmarginv
+ \labelwidth\leftmarginv
+ \advance\labelwidth-\labelsep}
+\def\@listvi {\leftmargin\leftmarginvi
+ \labelwidth\leftmarginvi
+ \advance\labelwidth-\labelsep}
+%
+% End of the "size9.clo" commands
+%**********************************************************************
+
+%
+% here's a few things that I didn't find in either article.cls or
+% size10.clo, so I left them here. --DAB
+%
+\setlength\columnsep{2pc} % Space between columns
+\setlength\columnseprule{0\p@} % Width of rule between columns.
+\hfuzz 1pt % Allow some variation in column width, otherwise it's
+ % too hard to typeset in narrow columns.
+
+
+%**********************************************************************
+%
+% Now we get on with overriding things found in article.cls
+%
+\setlength\parindent{13.5\p@}
+
+%
+% This command is used to format section headings. The format is the only
+% thing that differs between these section commands and the ones in
+% article.cls.
+%
+% Although the original documentation says that sans-serif is supposed to be
+% used for section titles, the file as I received uses roman. The
+% commented out line implements sans-serif. Be sure to comment out the
+% \bfseries line if you switch.
+% --DAB
+%
+\newcommand\@acmtitlestyle{\normalsize\bfseries}
+%\newcommand\@acmtitlestyle{\normalsize\sffamily}
+
+\renewcommand\section{\@startsection {section}{1}{\z@}%
+ {-3.5ex \@plus -1ex \@minus -.2ex}%
+ {2.3ex \@plus .2ex}%
+ {\@acmtitlestyle}}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
+ {-3.25ex \@plus -1ex \@minus -.2ex}%
+ {1.5ex \@plus .2ex}%
+ {\@acmtitlestyle}}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+ {-3.25ex \@plus -1ex \@minus -.2ex}%
+ {1.5ex \@plus .2ex}%
+ {\@acmtitlestyle}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
+ {3.25ex \@plus 1ex \@minus .2ex}%
+ {-1em}%
+ {\@acmtitlestyle}}
+\renewcommand\subparagraph{\@startsection{subparagraph}{4}{\parindent}%
+ {3.25ex \@plus 1ex \@minus .2ex}%
+ {-1em}%
+ {\@acmtitlestyle}}
+
+\setcounter{secnumdepth}{3}
+
+\setlength\arraycolsep{4.5\p@}
+\setlength\tabcolsep{5.4\p@}
+\setlength\doublerulesep{1.8\p@}
+
+\setlength\fboxsep{2.7\p@}
+\setlength\fboxrule{.4\p@}
+
+\def\tableofcontents{\ClassError{acmconf}%
+ {\protect\tableofcontents: Tables of contents are not allowed in the `acmconf' document class}%
+ {Remove the \protect\tableofcontents\space command from the file}}
+
+\def\listoffigures{\ClassError{acmconf}%
+ {\protect\listoffigures: Lists of figures are not allowed in the `acmconf' document class}%
+ {Remove the \protect\listoffigures\space command from the file}}
+
+\def\listoftables{\ClassError{acmconf}%
+ {\protect\listoftables: Lists of tables are not allowed in the `acmconf' document class}%
+ {Remove the \protect\listoftables\space command from the file}}
+\let\l@table\l@figure
+
+%
+% Added \@makefntext definition so that the mark would not over print
+% the beginning of the \thanks text. --DAB
+%
+\def\maketitle{\par
+ \begingroup
+ \def\thefootnote{\fnsymbol{footnote}}%
+ \def\@makefnmark{\hbox to 0pt{$\m@th^{\@thefnmark}$\hss}}%
+ \long\def\@makefntext##1{\parindent 1em\noindent
+ \hbox to1.8em{\hss$\m@th^{\@thefnmark}$}##1}%
+ \if@twocolumn
+ \twocolumn[\@maketitle]
+ \else \newpage
+ \global\@topnum\z@ % Prevents figures from going at top of page.
+ \@maketitle \fi
+ \thispagestyle{plain}\@thanks % UE: Changed {empty} to {plain}
+ \endgroup
+ \setcounter{footnote}{0}
+ \let\maketitle\relax
+ \let\@maketitle\relax
+ \gdef\@thanks{}\gdef\@author{}\gdef\@title{}\gdef\@affili{}\let\thanks\relax}
+
+%
+% extra declarations needed for our version of @maketitle
+%
+\newbox\@acmtitlebox
+\gdef\affili{}
+\def\affiliation#1{\gdef\affili{#1}}
+
+%
+% The modified @maketitle
+%
+\def\@maketitle{\newpage
+ \null
+ \setbox\@acmtitlebox\vbox{%
+ \vskip 2em % Vertical space above title.
+ \begin{center}
+ {\LARGE \@title \par} % Title set in \LARGE size.
+ \vskip 1.5em % Vertical space after title.
+ {\large % each author set in \large, in a
+ \lineskip .5em % tabular environment
+ \begin{tabular}[t]{c}\@author
+ \end{tabular}\par}
+ \vskip 1em
+ \begin{center}
+ {\large \affili}
+ \end{center}
+ \vskip 1.5em % Vertical space after author.
+ \end{center}}
+ \dimen0=\ht\@acmtitlebox
+ \advance\dimen0 by -13.5pc\relax
+ \unvbox\@acmtitlebox
+ \ifdim\dimen0<0.0pt\relax\vskip-\dimen0\fi}
+
+\long\def\unmarkedfootnote#1{{\long\def\@makefntext##1{##1}\footnotetext{#1}}}
+
+%% Use one of \copyrightspace or \toappear{To appear in the ACM ...}
+\def\copyrightspace{\unmarkedfootnote{\vrule height 4.5pc
+ width 0in depth 0in}}
+
+%% \small is bigger than \footnotesize.
+\def\toappear#1%
+ {\ifpreprint \unmarkedfootnote{\vrule height 2.25pc%
+ depth 2.25pc width 0in%
+ \parbox{2.8in}{\small #1}}%
+ \else \copyrightspace \fi}
+
+\def\marginpar{\ClassError{acmconf}%
+ {The \protect\marginpar command is not allowed in the `acmconf' document class}%
+ {Remove the \protect\marginpar\space command from the file}}
+
+\mark{{}{}} % Initializes TeX's marks
+
+%% Headings are ignored unless the [preprint] option is in force.
+\ifpreprint\else % preprint off -- all \pagestyle commands ==> \pagestyle{empty}.
+% \let\ps@plain\ps@empty % UE: Commented this line out
+ \let\ps@headings\ps@empty
+ \let\ps@myheadings\ps@empty
+\fi
+
+\raggedbottom % Ragged bottom
+
+\endinput
+%%
+%% End of file `acmconf.cls'.
--- a/Paper/document/acmconf.sty Wed Mar 17 20:42:42 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,737 +0,0 @@
-% ACMCONF DOCUMENT STYLE - Updated 17 August 1995.
-%
-% This is a patched version of the 5 April 1993 release. No stylistic changes
-% have been made; it should produce output identical to the 1993 release if
-% that release worked properly on your system. A LaTeX2e patch has been added
-% for systems having problems with the section header font. There is also a
-% macro for producing an ACM copyright notice and a box with reprint info.
-%
-% If you get an error message similar to
-%
-% ! Undefined control sequence.
-% l.165 \font\ninsfb = cmssbx10\@ptscale
-%
-% then see the comments beginning on line 173 (look for "DIAGNOSTICS").
-%-----------------------------------------------------------------------
-% Modification of Traub/Shivers version by Kevin Theobald, McGill
-% University. New version has automatic copyright space, option
-% for box around "to appear" entry, and style option to indent
-% first paragraph after subheadings. Released 5 April 1993.
-%
-% To use: install in reachable directory (one contained in TEXINPUTS
-% environment variable); use \documentstyle[<options>]{acmconf}
-%-----------------------------------------------------------------------
-% adapted from ARTICLE document style by Ken Traub
-% Hacked for [preprint] option by Olin Shivers 4/91
-% ARTICLE DOCUMENT STYLE -- Released 16 March 1988
-% for LaTeX version 2.09
-% Copyright (C) 1988 by Leslie Lamport
-
-%%% ACMCONF is a document style for producing two-column camera-ready pages for
-%%% ACM conferences, according to ACM specifications. The main features of
-%%% this style are:
-%%%
-%%% 1) Two columns.
-%%% 2) Side and top margins of 4.5pc, bottom margin of 6pc, column gutter of
-%%% 2pc, hence columns are 20pc wide and 55.5pc tall. (6pc = 1in, approx)
-%%% 3) First page has title information, and an extra 6pc of space at the
-%%% bottom of the first column for the ACM copyright notice.
-%%% 4) Text is 9pt on 10pt baselines; titles (except main) are 9pt bold.
-%%%
-%%% This document style supports a [preprint] style option that allows
-%%% you to run off a copy for a preprint -- with page numbers, "to
-%%% appear" information, and so forth. This is documented below.
-%%%
-%%% This document style also supports a [secindent] style option which
-%%% causes paragraphs following (sub)section heads to be indented like
-%%% the others. (Added by KBT)
-%%%
-%%% Finally, the macro \acmcopy{y} (y is year, e.g., 1995) prints the text of
-%%% an ACM copyright notice. This is useful for making a copy of the paper on
-%%% the author's FTP site (ACM requires a copyright notice). (Added by KBT)
-%%%
-%%% There are a few restrictions you must observe:
-%%%
-%%% 1) You cannot change the font size; ACM wants you to use 9pt.
-%%% 3) You must start your paper with the \maketitle command. Prior to the
-%%% \maketitle you must have \title and \author commands. If you have a
-%%% \date command it will be ignored; no date appears on the paper, since
-%%% the proceedings will have a date on the front cover.
-%%% 4) Marginal paragraphs, tables of contents, lists of figures and tables,
-%%% and page headings are all forbidden.
-%%% 5) The `figure' environment will produce a figure one column wide; if you
-%%% want one that is two columns wide, use `figure*'.
-%%%
-%%% Page Headings:
-%%% Normally, \pagestyle commands are ignored --- pages have no headings or
-%%% numbers. ACM will number the pages for you when they are inserted into the
-%%% proceedings (you should put page numbers on the BACK of each page, in
-%%% light pencil, in case someone drops your paper on the floor).
-%%%
-%%% If the [preprint] option is present, then \pagestyle commands are obeyed,
-%%% and the default is \pagestyle{plain}. All pages (including the first)
-%%% are numbered. (This is useful if you want to make a reprint version
-%%% of your paper, with page numbering identical to the conference
-%%% proceedings. In such a case, you may need to insert the command
-%%% \setcounter{page}{...} before \maketitle.) The [twoside] option is
-%%% also useful when using headers.
-%%%
-%%% Copyright Space:
-%%% This style automatically leaves 1" blank space at the bottom of page 1/
-%%% column 1. This space can optionally be filled with some text using the
-%%% \toappear{...} command. If used, this command must be BEFORE the \maketitle
-%%% command. If this command is defined AND [preprint] is on, then the
-%%% space is filled with the {...} text (at the bottom); otherwise, it is
-%%% blank. If you use \toappearbox{...} instead of \toappear{...} then a
-%%% box will be drawn around the text (if [preprint] is on).
-%%%
-%%% A typical usage looks like this:
-%%% \toappear{To appear in the Ninth AES Conference on Medievil Lithuanian
-%%% Embalming Technique, June 1991, Alfaretta, Georgia.}
-%%% This will be included in the preprint, and left out of the conference
-%%% version.
-%%%
-%%% Acmconf defines two useful conditionals.
-%%% - \ifacmconf{true-stuff}{false-stuff}
-%%% expands to true-stuff.
-%%% - \ifpreprint true-stuff \else else-stuff \fi
-%%% expands to true-stuff if the [preprint] option is being used,
-%%% otherwise it expands to else-stuff.
-%%% \ifacmconf is a latex command; \ifpreprint is a real latex conditional.
-%%%
-%%% WARNING:
-%%% Some dvi-ps converters heuristically allow chars to drift from their
-%%% true positions a few pixels. This loses noticeably with the 9pt sans-serif
-%%% bold font used for section headers. You turn this hackery off in our
-%%% dvi-ps converters with the -e option:
-%%% dvips -e 0 foo.dvi >foo.ps
-
-\typeout{Document Style `acmconf' <22 May 89>. Hacked 4/91 by}
-\typeout{ shivers@cs.cmu.edu, 4/93 by theobald@cs.mcgill.ca}
-\typeout{Bugs to theobald@cs.mcgill.ca}
-
-\def\acmcopy#1{Copyright \copyright {#1} by the Association for Computing
-Machinery, Inc. Permission to make digital or hard copies of part or all of
-this work for personal or classroom use is granted without fee provided that
-copies are not made or distributed for profit or direct commercial advantage
-and that copies bear this notice and the full citation on the first page.
-Copyrights for components of this work owned by others than ACM must be
-honored. Abstracting with credit is permitted. To copy otherwise, to
-republish, to post on servers, or to redistribute to lists, requires prior
-specific permission and/or a fee. Request permissions from Publications
-Dept., ACM Inc., fax +1 (212) 869-0481, or (permissions@acm.org).}
-
-\newif\if@acmconf\@acmconftrue
-\long\def\ifacmconf#1#2{\if@acmconf#1\else#2\fi}
-
-\newif\ifpreprint
-\def\ds@preprint{\preprinttrue}
-\def\ds@twoside{\@twosidetrue \@mparswitchtrue}
-\def\ds@secindent{\def\@afterindentfalse{\@afterindenttrue}}
-
-%
-% The following macro added 8/17/95 by KBT. Use to make box above title with
-% name of proceedings and/or copyright notice. This box is created only if
-% [preprint] is on. Use: \coverbox{vert. pos.}{horiz. pos.}{box width}{text}
-% Creates box with officially zero dimension, so does not affect layout.
-%
-\def\coverbox#1#2#3#4{\ifpreprint{\makebox[0pt][l]{\raisebox{#1}[0pt][0pt]{\hspace*{#2}\fbox{\parbox{#3}{#4}}}}}\else{}\fi}
-
-\@namedef{ds@10pt}{\@latexerr{The `10pt' option is not allowed in the `acmconf'
- document style.}\@eha}
-\@namedef{ds@11pt}{\@latexerr{The `11pt' option is not allowed in the `acmconf'
- document style.}\@eha}
-\@namedef{ds@12pt}{\@latexerr{The `12pt' option is not allowed in the `acmconf'
- document style.}\@eha}
-
-\@options
-
-\lineskip 1pt % \lineskip is 1pt for all font sizes.
-\normallineskip 1pt
-\def\baselinestretch{1}
-
-\def\@normalsize{\@setsize\normalsize{10pt}\ixpt\@ixpt
-\abovedisplayskip 9pt plus2pt minus4.5pt%
-\belowdisplayskip \abovedisplayskip
-\abovedisplayshortskip \z@ plus3pt%
-\belowdisplayshortskip 5.4pt plus3pt minus3pt%
-\let\@listi\@listI} % Setting of \@listi added 9 Jun 87
-
-\def\small{\@setsize\small{9pt}\viiipt\@viiipt
-\abovedisplayskip 7.6pt plus 3pt minus 4pt%
-\belowdisplayskip \abovedisplayskip
-\abovedisplayshortskip \z@ plus2pt%
-\belowdisplayshortskip 3.6pt plus2pt minus 2pt
-\def\@listi{\leftmargin\leftmargini %% Added 22 Dec 87
-\topsep 4pt plus 2pt minus 2pt\parsep 2pt plus 1pt minus 1pt
-\itemsep \parsep}}
-
-\def\footnotesize{\@setsize\footnotesize{8pt}\viipt\@viipt
-\abovedisplayskip 6.4pt plus 2pt minus 4pt%
-\belowdisplayskip \abovedisplayskip
-\abovedisplayshortskip \z@ plus 1pt%
-\belowdisplayshortskip 2.7pt plus 1pt minus 2pt
-\def\@listi{\leftmargin\leftmargini %% Added 22 Dec 87
-\topsep 3pt plus 1pt minus 1pt\parsep 2pt plus 1pt minus 1pt
-\itemsep \parsep}}
-
-\def\scriptsize{\@setsize\scriptsize{8pt}\viipt\@viipt}
-\def\tiny{\@setsize\tiny{6pt}\vpt\@vpt}
-\def\large{\@setsize\large{13.6pt}\xipt\@xipt}
-\def\Large{\@setsize\Large{16pt}\xiipt\@xiipt}
-\def\LARGE{\@setsize\LARGE{18pt}\xivpt\@xivpt}
-\def\huge{\@setsize\huge{22pt}\xviipt\@xviipt}
-\def\Huge{\@setsize\Huge{25pt}\xxpt\@xxpt}
-
-%%% Patch for LaTeX-2e (LaTeX 2.09 compatibility mode)
-%%% The line \font\ninsfb = cmssbx10\@ptscale9 is replaced by
-\expandafter\ifx\csname fontseries\endcsname\relax
- \font\ninsfb = cmssbx10\@ptscale9
- \else
- \def\ninsfb{\fontfamily{cmss}\fontseries{bx}\fontshape{n}
- \fontsize{9}{\f@baselineskip}\selectfont}
-\fi
-%%% End patch for LaTeX-2e
-\def\@acmtitlestyle{\normalsize\ninsfb}
-%%%
-%%% DIAGNOSTICS:
-%%% The ten lines above (the patch and the \def\@acmtitlestyle command) will
-%%% cause problems if your printer doesn't have the 9pt. bold sans-serif font.
-%%% If this is a problem, try commenting out those lines and uncommenting one
-%%% of the following alternatives. (It is best to try them in order until
-%%% finding one that works; the earlier alternatives cause less change.)
-%%%
-%%% ALTERNATIVE 1: (works if your system has the same font in 10pt.)
-%%% \font\tensfb = cmssbx10
-%%% \def\@acmtitlestyle{\normalsize\tensfb}
-%%% ALTERNATIVE 2:
-%%% \def\@acmtitlestyle{\normalsize\ninbf}
-%%% ALTERNATIVE 3:
-%%% \def\@acmtitlestyle{\normalsize\tenbf}
-
-\normalsize % Choose the normalsize font.
-
-\oddsidemargin 4.5pc
-\evensidemargin 4.5pc
-\advance\oddsidemargin by -1in % Correct for LaTeX gratuitousness
-\advance\evensidemargin by -1in % Correct for LaTeX gratuitousness
-\marginparwidth 0pt % Margin pars are not allowed.
-\marginparsep 11pt % Horizontal space between outer margin and
- % marginal note
-
- % Top of page:
-\topmargin 4.5pc % Nominal distance from top of page to top of
- % box containing running head.
-\advance\topmargin by -1in % Correct for LaTeX gratuitousness
-\headheight 0pt % Height of box containing running head.
-\headsep 0pt % Space between running head and text.
- % Bottom of page:
-\footskip 30pt % Distance from baseline of box containing foot
- % to baseline of last line of text.
-\footheight 12pt % Height of box containing running foot.
-
-%% Must redefine the top margin so there's room for headers and
-%% page numbers if you are using the preprint option. Footers
-%% are OK as is. Olin.
-\advance\topmargin by -37pt % Leave 37pt above text for headers
-\headheight 12pt % Height of box containing running head.
-\headsep 25pt % Space between running head and text.
-
-\textheight 666pt % 9 1/4 column height
-\textwidth 42pc % Width of text line.
- % For two-column mode:
-\columnsep 2pc % Space between columns
-\columnseprule 0pt % Width of rule between columns.
-\hfuzz 1pt % Allow some variation in column width, otherwise it's
- % too hard to typeset in narrow columns.
-
-\footnotesep 5.6pt % Height of strut placed at the beginning of every
- % footnote = height of normal \footnotesize strut,
- % so no extra space between footnotes.
-
-\skip\footins 8.1pt plus 4pt minus 2pt % Space between last line of text and
- % top of first footnote.
-\floatsep 11pt plus 2pt minus 2pt % Space between adjacent floats moved
- % to top or bottom of text page.
-\textfloatsep 18pt plus 2pt minus 4pt % Space between main text and floats
- % at top or bottom of page.
-\intextsep 11pt plus 2pt minus 2pt % Space between in-text figures and
- % text.
-\@maxsep 18pt % The maximum of \floatsep,
- % \textfloatsep and \intextsep (minus
- % the stretch and shrink).
-\dblfloatsep 11pt plus 2pt minus 2pt % Same as \floatsep for double-column
- % figures in two-column mode.
-\dbltextfloatsep 18pt plus 2pt minus 4pt% \textfloatsep for double-column
- % floats.
-\@dblmaxsep 18pt % The maximum of \dblfloatsep and
- % \dbltexfloatsep.
-\@fptop 0pt plus 1fil % Stretch at top of float page/column. (Must be
- % 0pt plus ...)
-\@fpsep 8pt plus 2fil % Space between floats on float page/column.
-\@fpbot 0pt plus 1fil % Stretch at bottom of float page/column. (Must be
- % 0pt plus ... )
-\@dblfptop 0pt plus 1fil % Stretch at top of float page. (Must be 0pt plus ...)
-\@dblfpsep 8pt plus 2fil % Space between floats on float page.
-\@dblfpbot 0pt plus 1fil % Stretch at bottom of float page. (Must be
- % 0pt plus ... )
-\marginparpush 5pt % Minimum vertical separation between two marginal
- % notes.
-
-\parskip 0pt plus 1pt % Extra vertical space between paragraphs.
-\parindent 13.5pt % Width of paragraph indentation.
-%\topsep 8pt plus 2pt minus 4pt % Extra vertical space, in addition to
- % \parskip, added above and below list and
- % paragraphing environments.
-\partopsep 2pt plus 1pt minus 1pt% Extra vertical space, in addition to
- % \parskip and \topsep, added when user
- % leaves blank line before environment.
-%\itemsep 4pt plus 2pt minus 1pt % Extra vertical space, in addition to
- % \parskip, added between list items.
-% See \@listI for values of \topsep and \itemsep
-
-\@lowpenalty 51 % Produced by \nopagebreak[1] or \nolinebreak[1]
-\@medpenalty 151 % Produced by \nopagebreak[2] or \nolinebreak[2]
-\@highpenalty 301 % Produced by \nopagebreak[3] or \nolinebreak[3]
-
-\@beginparpenalty -\@lowpenalty % Before a list or paragraph environment.
-\@endparpenalty -\@lowpenalty % After a list or paragraph environment.
-\@itempenalty -\@lowpenalty % Between list items.
-
-% \clubpenalty % 'Club line' at bottom of page.
-% \widowpenalty % 'Widow line' at top of page.
-% \displaywidowpenalty % Math display widow line.
-% \predisplaypenalty % Breaking before a math display.
-% \postdisplaypenalty % Breaking after a math display.
-% \interlinepenalty % Breaking at a line within a paragraph.
-% \brokenpenalty % Breaking after a hyphenated line.
-
-\def\part{\par % New paragraph
- \addvspace{4ex} % Adds vertical space above title.
- \@afterindentfalse % Suppresses indent in first paragraph. Change
- \secdef\@part\@spart}% to \@afterindenttrue to have indent.
-
-\def\@part[#1]#2{\ifnum \c@secnumdepth >\m@ne % IF secnumdepth > -1
- \refstepcounter{part} % THEN step part counter
- \addcontentsline{toc}{part}{\thepart % add toc line
- \hspace{1em}#1}\else % ELSE add unnumbered line
- \addcontentsline{toc}{part}{#1}\fi % FI
- { \parindent 0pt \raggedright
- \ifnum \c@secnumdepth >\m@ne% IF secnumdepth > -1
- \Large \bf Part \thepart % THEN Print 'Part' and
- \par \nobreak % number in \Large boldface.
- \fi % FI
- \huge \bf % Select \huge boldface.
- #2\markboth{}{}\par } % Print title and set heading marks null.
- \nobreak % TeX penalty to prevent page break.
- \vskip 3ex % Space between title and text.
- \@afterheading % Routine called after part and
- } % section heading.
-
-\def\@spart#1{{\parindent 0pt \raggedright
- \huge \bf
- #1\par} % Title.
- \nobreak % TeX penalty to prevent page break.
- \vskip 3ex % Space between title and text.
- \@afterheading % Routine called after part and
- } % section heading.
-
-\def\section{\@startsection {section}{1}{\z@}{-3.5ex plus -1ex minus
- -.2ex}{2.3ex plus .2ex}{\@acmtitlestyle}}
-\def\subsection{\@startsection{subsection}{2}{\z@}{-3.25ex plus -1ex minus
- -.2ex}{1.5ex plus .2ex}{\@acmtitlestyle}}
-\def\subsubsection{\@startsection{subsubsection}{3}{\z@}{-3.25ex plus
--1ex minus -.2ex}{1.5ex plus .2ex}{\@acmtitlestyle}}
-\def\paragraph{\@startsection
- {paragraph}{4}{\z@}{3.25ex plus 1ex minus .2ex}{-1em}{\@acmtitlestyle}}
-\def\subparagraph{\@startsection
- {subparagraph}{4}{\parindent}{3.25ex plus 1ex minus
- .2ex}{-1em}{\@acmtitlestyle}}
-
-\setcounter{secnumdepth}{3}
-
-\def\appendix{\par
- \setcounter{section}{0}
- \setcounter{subsection}{0}
- \def\thesection{\Alph{section}}}
-
-\leftmargini 22.5pt
-\leftmarginii 19.8pt % > \labelsep + width of '(m)'
-\leftmarginiii 16.8pt % > \labelsep + width of 'vii.'
-\leftmarginiv 15.3pt % > \labelsep + width of 'M.'
-\leftmarginv 9pt
-\leftmarginvi 9pt
-
-\leftmargin\leftmargini
-\labelsep 4.5pt
-\labelwidth\leftmargini\advance\labelwidth-\labelsep
-% \parsep 4pt plus 2pt minus 1pt (Removed 9 Jun 87)
-
-% \@listI defines top level and \@listi values of
-% \leftmargin, \topsep, \parsep, and \itemsep
-% (Added 9 Jun 87)
-\def\@listI{\leftmargin\leftmargini \parsep 3.6pt plus 2pt minus 1pt%
-\topsep 7.2pt plus 2pt minus 4pt%
-\itemsep 3.6pt plus 2pt minus 1pt}
-
-\let\@listi\@listI
-\@listi
-
-\def\@listii{\leftmargin\leftmarginii
- \labelwidth\leftmarginii\advance\labelwidth-\labelsep
- \topsep 3.6pt plus 2pt minus 1pt
- \parsep 1.8pt plus 0.9pt minus 0.9pt
- \itemsep \parsep}
-
-\def\@listiii{\leftmargin\leftmarginiii
- \labelwidth\leftmarginiii\advance\labelwidth-\labelsep
- \topsep 1.8pt plus 0.9pt minus 0.9pt
- \parsep \z@ \partopsep 1pt plus 0pt minus 1pt
- \itemsep \topsep}
-
-\def\@listiv{\leftmargin\leftmarginiv
- \labelwidth\leftmarginiv\advance\labelwidth-\labelsep}
-
-\def\@listv{\leftmargin\leftmarginv
- \labelwidth\leftmarginv\advance\labelwidth-\labelsep}
-
-\def\@listvi{\leftmargin\leftmarginvi
- \labelwidth\leftmarginvi\advance\labelwidth-\labelsep}
-
-\def\labelenumi{\theenumi.}
-\def\theenumi{\arabic{enumi}}
-
-\def\labelenumii{(\theenumii)}
-\def\theenumii{\alph{enumii}}
-\def\p@enumii{\theenumi}
-
-\def\labelenumiii{\theenumiii.}
-\def\theenumiii{\roman{enumiii}}
-\def\p@enumiii{\theenumi(\theenumii)}
-
-\def\labelenumiv{\theenumiv.}
-\def\theenumiv{\Alph{enumiv}}
-\def\p@enumiv{\p@enumiii\theenumiii}
-
-\def\labelitemi{$\bullet$}
-\def\labelitemii{\bf --}
-\def\labelitemiii{$\ast$}
-\def\labelitemiv{$\cdot$}
-
-\def\verse{\let\\=\@centercr
- \list{}{\itemsep\z@ \itemindent -1.5em\listparindent \itemindent
- \rightmargin\leftmargin\advance\leftmargin 1.5em}\item[]}
-\let\endverse\endlist
-
-\def\quotation{\list{}{\listparindent 1.5em
- \itemindent\listparindent
- \rightmargin\leftmargin \parsep 0pt plus 1pt}\item[]}
-\let\endquotation=\endlist
-
-\def\quote{\list{}{\rightmargin\leftmargin}\item[]}
-\let\endquote=\endlist
-
-\def\descriptionlabel#1{\hspace\labelsep \bf #1}
-\def\description{\list{}{\labelwidth\z@ \itemindent-\leftmargin
- \let\makelabel\descriptionlabel}}
-
-\let\enddescription\endlist
-
-%\newdimen\descriptionmargin
-%\descriptionmargin=3em
-
-\def\theequation{\arabic{equation}}
-
-% \jot = 3pt % Extra space added between lines of an eqnarray environment
-
-% The macro \@eqnnum defines how equation numbers are to appear in equations.
-%
-% \def\@eqnnum{(\theequation)}
-%
-
-% Changed pagenum to 1, so margins work right in twoside option.
-% It's not clear to me that this environment is useful for acmconf.sty
-% anyway. -Olin
-\def\titlepage{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
- \else \newpage \fi \thispagestyle{empty}\c@page\@ne}
-
-\def\endtitlepage{\if@restonecol\twocolumn \else \newpage \fi \c@page\@ne}
-
-\arraycolsep 4.5pt % Half the space between columns in an array environment.
-\tabcolsep 5.4pt % Half the space between columns in a tabular environment.
-\arrayrulewidth .4pt % Width of rules in array and tabular environment.
-\doublerulesep 1.8pt % Space between adjacent rules in array or tabular env.
-
-\tabbingsep \labelsep % Space used by the \' command. (See LaTeX manual.)
-
-\skip\@mpfootins = \skip\footins
-
-\fboxsep = 2.7pt % Space left between box and text by \fbox and \framebox.
-\fboxrule = .4pt % Width of rules in box made by \fbox and \framebox.
-
-\newcounter{part}
-\newcounter {section}
-\newcounter {subsection}[section]
-\newcounter {subsubsection}[subsection]
-\newcounter {paragraph}[subsubsection]
-\newcounter {subparagraph}[paragraph]
-
-\def\thepart{\Roman{part}} % Roman numeral part numbers.
-\def\thesection {\arabic{section}}
-\def\thesubsection {\thesection.\arabic{subsection}}
-\def\thesubsubsection {\thesubsection .\arabic{subsubsection}}
-\def\theparagraph {\thesubsubsection.\arabic{paragraph}}
-\def\thesubparagraph {\theparagraph.\arabic{subparagraph}}
-
-\def\@pnumwidth{1.55em}
-\def\@tocrmarg {2.55em}
-\def\@dotsep{4.5}
-\setcounter{tocdepth}{3}
-
-\def\tableofcontents{\@latexerr{\tableofcontents: Tables of contents are not
- allowed in the `acmconf' document style.}\@eha}
-
-\def\l@part#1#2{\addpenalty{\@secpenalty}
- \addvspace{2.25em plus 1pt} % space above part line
- \begingroup
- \@tempdima 3em % width of box holding part number, used by
- \parindent \z@ \rightskip \@pnumwidth %% \numberline
- \parfillskip -\@pnumwidth
- {\large \bf % set line in \large boldface
- \leavevmode % TeX command to enter horizontal mode.
- #1\hfil \hbox to\@pnumwidth{\hss #2}}\par
- \nobreak % Never break after part entry
- \endgroup}
-
-\def\l@section#1#2{\addpenalty{\@secpenalty} % good place for page break
- \addvspace{1.0em plus 1pt} % space above toc entry
- \@tempdima 1.5em % width of box holding section number
- \begingroup
- \parindent \z@ \rightskip \@pnumwidth
- \parfillskip -\@pnumwidth
- \bf % Boldface.
- \leavevmode % TeX command to enter horizontal mode.
- \advance\leftskip\@tempdima %% added 5 Feb 88 to conform to
- \hskip -\leftskip %% 25 Jan 88 change to \numberline
- #1\nobreak\hfil \nobreak\hbox to\@pnumwidth{\hss #2}\par
- \endgroup}
-
-
-\def\l@subsection{\@dottedtocline{2}{1.5em}{2.3em}}
-\def\l@subsubsection{\@dottedtocline{3}{3.8em}{3.2em}}
-\def\l@paragraph{\@dottedtocline{4}{7.0em}{4.1em}}
-\def\l@subparagraph{\@dottedtocline{5}{10em}{5em}}
-
-\def\listoffigures{\@latexerr{\listoffigures: Lists of figures are not
- allowed in the `acmconf' document style.}\@eha}
-
-\def\l@figure{\@dottedtocline{1}{1.5em}{2.3em}}
-
-\def\listoftables{\@latexerr{\listoftables: Lists of tables are not
- allowed in the `acmconf' document style.}\@eha}
-\let\l@table\l@figure
-
-
-\def\thebibliography#1{\section*{References\@mkboth
- {REFERENCES}{REFERENCES}}\list
- {[\arabic{enumi}]}{\settowidth\labelwidth{[#1]}\leftmargin\labelwidth
- \advance\leftmargin\labelsep
- \usecounter{enumi}}
- \def\newblock{\hskip .11em plus .33em minus .07em}
- \sloppy\clubpenalty4000\widowpenalty4000
- \sfcode`\.=1000\relax}
-
-\let\endthebibliography=\endlist
-
-% \def\@biblabel#1{[#1]\hfill} % Produces the label for a \bibitem[...]
- % command.
-% \def\@cite#1{[#1]} % Produces the output of the \cite command.
-
-\newif\if@restonecol
-
-\def\theindex{\@restonecoltrue\if@twocolumn\@restonecolfalse\fi
-\columnseprule \z@
-\columnsep 35pt\twocolumn[\section*{Index}]
- \@mkboth{INDEX}{INDEX}\thispagestyle{empty}\parindent\z@
- \parskip\z@ plus .3pt\relax\let\item\@idxitem}
-
-\def\@idxitem{\par\hangindent 40pt}
-
-\def\subitem{\par\hangindent 40pt \hspace*{20pt}}
-
-\def\subsubitem{\par\hangindent 40pt \hspace*{30pt}}
-
-\def\endtheindex{\if@restonecol\onecolumn\else\clearpage\fi}
-
-\def\indexspace{\par \vskip 10pt plus 5pt minus 3pt\relax}
-
-\def\footnoterule{\kern-3\p@
- \hrule width .4\columnwidth
- \kern 2.6\p@} % The \hrule has default height of .4pt .
-
-\long\def\@makefntext#1{\parindent 1em\noindent
- \hbox to 1.8em{\hss$^{\@thefnmark}$}#1}
-
-\setcounter{topnumber}{2}
-\def\topfraction{.7}
-\setcounter{bottomnumber}{1}
-\def\bottomfraction{.3}
-\setcounter{totalnumber}{3}
-\def\textfraction{.2}
-\def\floatpagefraction{.5}
-\setcounter{dbltopnumber}{2}
-\def\dbltopfraction{.7}
-\def\dblfloatpagefraction{.5}
-
-\long\def\@makecaption#1#2{
- \vskip 10pt
- \setbox\@tempboxa\hbox{#1: #2}
- \ifdim \wd\@tempboxa >\hsize % IF longer than one line:
- #1: #2\par % THEN set as ordinary paragraph.
- \else % ELSE center.
- \hbox to\hsize{\hfil\box\@tempboxa\hfil}
- \fi}
-
-\newcounter{figure}
-\def\thefigure{\@arabic\c@figure}
-
-\def\fps@figure{tbp}
-\def\ftype@figure{1}
-\def\ext@figure{lof}
-\def\fnum@figure{Figure \thefigure}
-\def\figure{\@float{figure}}
-\let\endfigure\end@float
-\@namedef{figure*}{\@dblfloat{figure}}
-\@namedef{endfigure*}{\end@dblfloat}
-
-\newcounter{table}
-\def\thetable{\@arabic\c@table}
-
-\def\fps@table{tbp}
-\def\ftype@table{2}
-\def\ext@table{lot}
-\def\fnum@table{Table \thetable}
-\def\table{\@float{table}}
-\let\endtable\end@float
-\@namedef{table*}{\@dblfloat{table}}
-\@namedef{endtable*}{\end@dblfloat}
-
-\def\maketitle{\par
- \begingroup
- \def\thefootnote{\fnsymbol{footnote}}
- \def\@makefnmark{\hbox
- to 0pt{$^{\@thefnmark}$\hss}}
- \if@twocolumn
- \twocolumn[\@maketitle]
- \else \newpage
- \global\@topnum\z@ % Prevents figures from going at top of page.
-% \@maketitle \fi\thispagestyle{empty}\@thanks
- \@maketitle \fi\@thanks
- \endgroup
- \setcounter{footnote}{0}
- \let\maketitle\relax
- \let\@maketitle\relax
- \gdef\@thanks{}\gdef\@author{}\gdef\@title{}\let\thanks\relax
- \@copyrightspace}
-
-\newbox\@acmtitlebox
-\def\@maketitle{\newpage
- \null
- \setbox\@acmtitlebox\vbox{%
- \vskip 2em % Vertical space above title.
- \begin{center}
- {\LARGE \@title \par} % Title set in \LARGE size.
- \vskip 1.5em % Vertical space after title.
- {\large % each author set in \large, in a
- \lineskip .5em % tabular environment
- \begin{tabular}[t]{c}\@author
- \end{tabular}\par}
- \vskip 1.5em % Vertical space after author.
- \end{center}}
- \dimen0=\ht\@acmtitlebox
- \advance\dimen0 by -14.5pc\relax % Increased space for title box -- KBT
- \unvbox\@acmtitlebox
- \ifdim\dimen0<0.0pt\relax\vskip-\dimen0\fi}
-
-\def\abstract{\if@twocolumn
-\section*{Abstract}
-\else \small
-\begin{center}
-{\bf Abstract\vspace{-.5em}\vspace{0pt}}
-\end{center}
-\quotation
-\fi}
-
-\def\endabstract{\if@twocolumn\else\endquotation\fi}
-
-%%% This section (written by KBT) handles the 1" box in the lower left
-%%% corner of the left column of the first page by creating a picture,
-%%% and inserting the predefined string at the bottom (with a negative
-%%% displacement to offset the space allocated for a non-existent
-%%% caption).
-%%%
-\def\ftype@copyrightbox{8}
-\def\@copyrightspace{
-\@float{copyrightbox}[b]
-\begin{center}
-\setlength{\unitlength}{1pc}
-\begin{picture}(20,2.8)
-\ifpreprint \put(0,-0.95){\@toappear} \else \fi
-\end{picture}
-\end{center}
-\end@float}
-
-\def\@toappear{} % Default setting blank - commands below change this.
-\def\toappear#1{\def\@toappear{\parbox[b]{20pc}{#1}}}
-\def\toappearbox#1{\def\@toappear{\raisebox{5pt}{\framebox[20pc]{\parbox[b]{19pc}{#1}}}}}
-
-\def\marginpar{\@latexerr{The \marginpar command is not allowed in the
- `acmconf' document style.}\@eha}
-
-\mark{{}{}} % Initializes TeX's marks
-
-%% Headings are ignored unless the [preprint] option is in force.
-\ifpreprint
- \if@twoside
- \def\ps@headings{
- \def\@oddfoot{}
- \def\@evenfoot{}
- \def\@evenhead{\rm\thepage\hfil \sl \leftmark}
- \def\@oddhead{\hbox{}\sl \rightmark \hfil\rm\thepage}
- \def\sectionmark##1{\markboth {\uppercase{\ifnum\c@secnumdepth>\z@
- \thesection \hskip 1em\relax \fi ##1}}{}}
- \def\subsectionmark##1
- {\markright {\ifnum \c@secnumdepth >\@ne \thesubsection
- \hskip 1em\relax \fi ##1}}}
-
- \else
- \def\ps@headings{
- \def\@oddfoot{}
- \def\@evenfoot{}
- \def\@oddhead{\hbox{}\sl \rightmark \hfil \rm\thepage}
- \def\sectionmark##1{\markright{\uppercase{\ifnum \c@secnumdepth >\z@
- \thesection\hskip 1em\relax \fi ##1}}}}
- \fi
-
- \def\ps@myheadings{\def\@oddhead{\hbox{}\sl\rightmark \hfil\rm\thepage}%
- \def \@evenhead{\rm \thepage\hfil\sl\leftmark\hbox{}}%
- \def\@oddfoot{}%
- \def\@evenfoot{}%
- \def\sectionmark##1{}%
- \def\subsectionmark##1{}}
-
-\else % preprint off -- all \pagestyle commands ==> \pagestyle{empty}.
- \let\ps@plain\ps@empty
- \let\ps@headings\ps@empty
- \let\ps@myheadings\ps@empty
-\fi
-
-\def\today{\ifcase\month\or
- January\or February\or March\or April\or May\or June\or
- July\or August\or September\or October\or November\or December\fi
- \space\number\day, \number\year}
-
-\ps@plain
-\pagenumbering{arabic} % Arabic page numbers
-\twocolumn % Double column.
-\raggedbottom % Ragged bottom
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/root.bib Thu Mar 18 00:17:21 2010 +0100
@@ -0,0 +1,131 @@
+@Unpublished{HuffmanUrban10,
+ author = {B.~Huffman and C.~Urban},
+ title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},
+ note = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
+ year = {2010}
+}
+
+@Unpublished{SatoPollack10,
+ author = {M.~Sato and R.~Pollack},
+ title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},
+ note = {To appear in {\it Journal of Symbolic Computation}}
+}
+
+@article{GabbayPitts02,
+ author = {M.~J.~Gabbay and A.~M.~Pitts},
+ title = {A New Approach to Abstract Syntax with Variable
+ Binding},
+ journal = {Formal Aspects of Computing},
+ volume = {13},
+ year = 2002,
+ pages = {341--363}
+}
+
+@article{Pitts03,
+ author = {A.~M.~Pitts},
+ title = {Nominal Logic, A First Order Theory of Names and
+ Binding},
+ journal = {Information and Computation},
+ year = {2003},
+ volume = {183},
+ pages = {165--193}
+}
+
+@InProceedings{BengtsonParrow07,
+ author = {J.~Bengtson and J.~Parrow},
+ title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic},
+ booktitle = {Proc.~of the 10th International Conference on
+ Foundations of Software Science and Computation Structures (FOSSACS)},
+ year = 2007,
+ pages = {63--77},
+ series = {LNCS},
+ volume = {4423}
+}
+
+@inproceedings{BengtsonParow09,
+ author = {J.~Bengtson and J.~Parrow},
+ title = {{P}si-{C}alculi in {I}sabelle},
+ booktitle = {Proc of the 22nd Conference on Theorem Proving in
+ Higher Order Logics (TPHOLs)},
+ year = 2009,
+ pages = {99--114},
+ series = {LNCS},
+ volume = {5674}
+}
+
+@inproceedings{TobinHochstadtFelleisen08,
+ author = {S.~Tobin-Hochstadt and M.~Felleisen},
+ booktitle = {Proc.~of the 35rd Symposium on
+ Principles of Programming Languages (POPL)},
+ title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme},
+ publisher = {ACM},
+ year = {2008},
+ pages = {395--406}
+}
+
+@InProceedings{UrbanCheneyBerghofer08,
+ author = "C.~Urban and J.~Cheney and S.~Berghofer",
+ title = "{M}echanizing the {M}etatheory of {LF}",
+ pages = "45--56",
+ year = 2008,
+ booktitle = "Proc.~of the 23rd IEEE Symposium on Logic in Computer Science (LICS)"
+}
+
+@InProceedings{UrbanZhu08,
+ title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof",
+ author = "C.~Urban and B.~Zhu",
+ booktitle = "Proc.~of the 9th International Conference on Rewriting Techniques
+ and Applications (RTA)",
+ year = "2008",
+ pages = "409--424",
+ series = "LNCS",
+ volume = 5117
+}
+
+@Article{UrbanPittsGabbay04,
+ title = "{N}ominal {U}nification",
+ author = "C.~Urban and A.M.~Pitts and M.J.~Gabbay",
+ journal = "Theoretical Computer Science",
+ pages = "473--497",
+ volume = "323",
+ number = "1-3",
+ year = "2004"
+}
+
+@Article{Church40,
+ author = {A.~Church},
+ title = {{A} {F}ormulation of the {S}imple {T}heory of {T}ypes},
+ journal = {Journal of Symbolic Logic},
+ year = {1940},
+ volume = {5},
+ number = {2},
+ pages = {56--68}
+}
+
+
+@Manual{PittsHOL4,
+ title = {{S}yntax and {S}emantics},
+ author = {A.~M.~Pitts},
+ note = {Part of the documentation for the HOL4 system.}
+}
+
+
+@book{PaulsonBenzmueller,
+ year={2009},
+ author={Benzm{\"u}ller, Christoph and Paulson, Lawrence C.},
+ title={Quantified Multimodal Logics in Simple Type Theory},
+ note={{http://arxiv.org/abs/0905.2435}},
+ series={{SEKI Report SR--2009--02 (ISSN 1437-4447)}},
+ publisher={{SEKI Publications}}
+}
+
+@Article{Cheney06,
+ author = {J.~Cheney},
+ title = {{C}ompleteness and {H}erbrand theorems for {N}ominal {L}ogic},
+ journal = {Journal of Symbolic Logic},
+ year = {2006},
+ volume = {71},
+ number = {1},
+ pages = {299--320}
+}
+
--- a/Paper/document/root.tex Wed Mar 17 20:42:42 2010 +0100
+++ b/Paper/document/root.tex Thu Mar 18 00:17:21 2010 +0100
@@ -1,41 +1,24 @@
\documentclass{acmconf}
-\usepackage{isabelle,isabellesym}
-
-\ConferenceShortName{ICFP}
-\ConferenceName{International Conference on Functional Programming}
-
-% further packages required for unusual symbols (see also
-% isabellesym.sty), use only when needed
-
-%\usepackage{amssymb}
- %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
- %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
- %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage[greek,english]{babel}
- %option greek for \<euro>
- %option english (default language) for \<guillemotleft>, \<guillemotright>
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
-%\usepackage[latin1]{inputenc}
- %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
- %\<threesuperior>, \<threequarters>, \<degree>
-
-%\usepackage[only,bigsqcap]{stmaryrd}
- %for \<Sqinter>
+%\ConferenceShortName{ICFP}
+%\ConferenceName{International Conference on Functional Programming}
-%\usepackage{eufrak}
- %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
- %for \<cent>, \<currency>
-
-% this should be the last package used
\usepackage{pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymiota}{}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+
+
% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}
@@ -51,7 +34,7 @@
\begin{document}
-\title{\LARGE\bf General Binding Structures in Nominal Isabelle, or How to
+\title{\LARGE\bf General Binding Structures in Nominal Isabelle,\\ or How to
Formalise Core-Haskell}
\maketitle
@@ -64,13 +47,16 @@
are important in formalisation ...
\end{abstract}
+%\begin{keywords}
+%Language formalisations, Isabelle/HOL, POPLmark
+%\end{keywords}
+
+
% generated text of all theories
\input{session}
-%\bibliographystyle{plain}
-% optional bibliography
-%\bibliographystyle{abbrv}
-%\bibliography{root}
+\bibliographystyle{plain}
+\bibliography{root}
\end{document}