# HG changeset patch # User Christian Urban # Date 1268867841 -3600 # Node ID 52f68b524fd28d8bfa27539646f4c3e238d57e12 # Parent 4908db645f989100251da3073932943de87b6d89 slightly more of the paper diff -r 4908db645f98 -r 52f68b524fd2 Paper/Paper.thy --- 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] "_ \ _ :: (\ \ \) list \ \ \ \"} + + \noindent + with a generic type in which @{text "\"} stands for the type of atoms + and @{text "\"} 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. diff -r 4908db645f98 -r 52f68b524fd2 Paper/document/acmconf.cls --- /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'. diff -r 4908db645f98 -r 52f68b524fd2 Paper/document/acmconf.sty --- 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[]{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 diff -r 4908db645f98 -r 52f68b524fd2 Paper/document/root.bib --- /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} +} + diff -r 4908db645f98 -r 52f68b524fd2 Paper/document/root.tex --- 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 \, \, \, \, \, \, - %\, \, \, \, \, - %\, \, \ - -%\usepackage[greek,english]{babel} - %option greek for \ - %option english (default language) for \, \ +\usepackage{isabelle} +\usepackage{isabellesym} +\usepackage{amsmath} +\usepackage{amssymb} -%\usepackage[latin1]{inputenc} - %for \, \, \, \, - %\, \, \ - -%\usepackage[only,bigsqcap]{stmaryrd} - %for \ +%\ConferenceShortName{ICFP} +%\ConferenceName{International Conference on Functional Programming} -%\usepackage{eufrak} - %for \ ... \, \ ... \ (also included in amssymb) - -%\usepackage{textcomp} - %for \, \ - -% 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}