From 50a9fd311cddc00b65b57745e85c6b12f2534b27 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 17 Mar 2018 00:23:47 -0400 Subject: [PATCH] clean up latex junk --- Wtypes.tex | 2 +- aliascnt.sty | 88 --- history.txt | 132 ----- intro.tex | 2 +- llncs.cls | 1208 -------------------------------------- llncsdoc.sty | 42 -- main.out | 31 + main.tex | 57 +- main.toc | 32 + readme.txt | 30 - remreset.sty | 38 -- splncs.bst | 1095 ---------------------------------- splncs03.bst | 1519 ------------------------------------------------ splncs_srt.bst | 1248 --------------------------------------- sprmindx.sty | 4 - 15 files changed, 83 insertions(+), 5445 deletions(-) delete mode 100644 aliascnt.sty delete mode 100644 history.txt delete mode 100644 llncs.cls delete mode 100644 llncsdoc.sty create mode 100644 main.out create mode 100644 main.toc delete mode 100644 readme.txt delete mode 100644 remreset.sty delete mode 100644 splncs.bst delete mode 100644 splncs03.bst delete mode 100644 splncs_srt.bst delete mode 100644 sprmindx.sty diff --git a/Wtypes.tex b/Wtypes.tex index 154f108..45c5844 100644 --- a/Wtypes.tex +++ b/Wtypes.tex @@ -53,7 +53,7 @@ \section{Reduction of inductive types to $\W$-types} 1\le\ell\quad \Gamma\vdash C:\alpha\to\U_\ell\\ \Gamma\vdash e:\forall x:\alpha.\; (\forall y:\alpha.\;r\;y\;x\to\acc_r\;y)\to (\forall y:\alpha.\;r\;y\;x\to C\;y)\to C\;x \end{matrix}}{\Gamma\vdash \rec_\acc\;e:\forall x:\alpha.\;\acc_r\;x\to C\;x}$$ -All of these could have been defined as inductive types in the sense of section \ref{inductive}: +All of these could have been defined as inductive types in the sense of section \ref{sec:inductive}: \begin{align*} \bot&:=\mu t:\P.\;0\\ \Sigma x:\alpha.\;\beta&:=\mu t:\U_{\max(\ell,\ell',1)}.\;(\mathsf{pair}:\forall x:\alpha.\;\beta\to t)\\ diff --git a/aliascnt.sty b/aliascnt.sty deleted file mode 100644 index 8b4e866..0000000 --- a/aliascnt.sty +++ /dev/null @@ -1,88 +0,0 @@ -%% -%% This is file `aliascnt.sty', -%% generated with the docstrip utility. -%% -%% The original source files were: -%% -%% aliascnt.dtx (with options: `package') -%% -%% This is a generated file. -%% -%% Project: aliascnt -%% Version: 2009/09/08 v1.3 -%% -%% Copyright (C) 2006, 2009 by -%% Heiko Oberdiek -%% -%% This work may be distributed and/or modified under the -%% conditions of the LaTeX Project Public License, either -%% version 1.3c of this license or (at your option) any later -%% version. This version of this license is in -%% http://www.latex-project.org/lppl/lppl-1-3c.txt -%% and the latest version of this license is in -%% http://www.latex-project.org/lppl.txt -%% and version 1.3 or later is part of all distributions of -%% LaTeX version 2005/12/01 or later. -%% -%% This work has the LPPL maintenance status "maintained". -%% -%% This Current Maintainer of this work is Heiko Oberdiek. -%% -%% This work consists of the main source file aliascnt.dtx -%% and the derived files -%% aliascnt.sty, aliascnt.pdf, aliascnt.ins, aliascnt.drv. -%% -\NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{aliascnt}% - [2009/09/08 v1.3 Alias counter (HO)]% -\newcommand*{\newaliascnt}[2]{% - \begingroup - \def\AC@glet##1{% - \global\expandafter\let\csname##1#1\expandafter\endcsname - \csname##1#2\endcsname - }% - \@ifundefined{c@#2}{% - \@nocounterr{#2}% - }{% - \expandafter\@ifdefinable\csname c@#1\endcsname{% - \AC@glet{c@}% - \AC@glet{the}% - \AC@glet{theH}% - \AC@glet{p@}% - \expandafter\gdef\csname AC@cnt@#1\endcsname{#2}% - \expandafter\gdef\csname cl@#1\expandafter\endcsname - \expandafter{\csname cl@#2\endcsname}% - }% - }% - \endgroup -} -\newcommand*{\aliascntresetthe}[1]{% - \@ifundefined{AC@cnt@#1}{% - \PackageError{aliascnt}{% - `#1' is not an alias counter% - }\@ehc - }{% - \expandafter\let\csname the#1\expandafter\endcsname - \csname the\csname AC@cnt@#1\endcsname\endcsname - }% -} -\newcommand*{\AC@findrootcnt}[1]{% - \@ifundefined{AC@cnt@#1}{% - #1% - }{% - \expandafter\AC@findrootcnt\csname AC@cnt@#1\endcsname - }% -} -\def\AC@patch#1{% - \expandafter\let\csname AC@org@#1reset\expandafter\endcsname - \csname @#1reset\endcsname - \expandafter\def\csname @#1reset\endcsname##1##2{% - \csname AC@org@#1reset\endcsname{##1}{\AC@findrootcnt{##2}}% - }% -} -\RequirePackage{remreset} -\AC@patch{addto} -\AC@patch{removefrom} -\endinput -%% -%% End of file `aliascnt.sty'. diff --git a/history.txt b/history.txt deleted file mode 100644 index a60ecac..0000000 --- a/history.txt +++ /dev/null @@ -1,132 +0,0 @@ -Version history for the LLNCS LaTeX2e class - - date filename version action/reason/acknowledgements ----------------------------------------------------------------------------- - 29.5.96 letter.txt beta naming problems (subject index file) - thanks to Dr. Martin Held, Salzburg, AT - - subjindx.ind renamed to subjidx.ind as required - by llncs.dem - - history.txt introducing this file - - 30.5.96 llncs.cls incompatibility with new article.cls of - 1995/12/20 v1.3q Standard LaTeX document class, - \if@openbib is no longer defined, - reported by Ralf Heckmann and Graham Gough - solution by David Carlisle - - 10.6.96 llncs.cls problems with fragile commands in \author field - reported by Michael Gschwind, TU Wien - - 25.7.96 llncs.cls revision a corrects: - wrong size of text area, floats not \small, - some LaTeX generated texts - reported by Michael Sperber, Uni Tuebingen - - 16.4.97 all files 2.1 leaving beta state, - raising version counter to 2.1 - - 8.6.97 llncs.cls 2.1a revision a corrects: - unbreakable citation lists, reported by - Sergio Antoy of Portland State University - -11.12.97 llncs.cls 2.2 "general" headings centered; two new elements - for the article header: \email and \homedir; - complete revision of special environments: - \newtheorem replaced with \spnewtheorem, - introduced the theopargself environment; - two column parts made with multicol package; - add ons to work with the hyperref package - -07.01.98 llncs.cls 2.2 changed \email to simply switch to \tt - -25.03.98 llncs.cls 2.3 new class option "oribibl" to suppress - changes to the thebibliograpy environment - and retain pure LaTeX codes - useful - for most BibTeX applications - -16.04.98 llncs.cls 2.3 if option "oribibl" is given, extend the - thebibliograpy hook with "\small", suggested - by Clemens Ballarin, University of Cambridge - -20.11.98 llncs.cls 2.4 pagestyle "titlepage" - useful for - compilation of whole LNCS volumes - -12.01.99 llncs.cls 2.5 counters of orthogonal numbered special - environments are reset each new contribution - -27.04.99 llncs.cls 2.6 new command \thisbottomragged for the - actual page; indention of the footnote - made variable with \fnindent (default 1em); - new command \url that copys its argument - - 2.03.00 llncs.cls 2.7 \figurename and \tablename made compatible - to babel, suggested by Jo Hereth, TU Darmstadt; - definition of \url moved \AtBeginDocument - (allows for url package of Donald Arseneau), - suggested by Manfred Hauswirth, TU of Vienna; - \large for part entries in the TOC - -16.04.00 llncs.cls 2.8 new option "orivec" to preserve the original - vector definition, read "arrow" accent - -17.01.01 llncs.cls 2.9 hardwired texts made polyglot, - available languages: english (default), - french, german - all are "babel-proof" - -20.06.01 splncs.bst public release of a BibTeX style for LNCS, - nobly provided by Jason Noble - -14.08.01 llncs.cls 2.10 TOC: authors flushleft, - entries without hyphenation; suggested - by Wiro Niessen, Imaging Center - Utrecht - -23.01.02 llncs.cls 2.11 fixed footnote number confusion with - \thanks, numbered institutes, and normal - footnote entries; error reported by - Saverio Cittadini, Istituto Tecnico - Industriale "Tito Sarrocchi" - Siena - -28.01.02 llncs.cls 2.12 fixed footnote fix ; error reported by - Chris Mesterharm, CS Dept. Rutgers - NJ - -28.01.02 llncs.cls 2.13 fixed the fix (programmer needs vacation) - -17.08.04 llncs.cls 2.14 TOC: authors indented, smart \and handling - for the TOC suggested by Thomas Gabel - University of Osnabrueck - -07.03.06 splncs.bst fix for BibTeX entries without year; patch - provided by Jerry James, Utah State University - -14.06.06 splncs_srt.bst a sorting BibTeX style for LNCS, feature - provided by Tobias Heindel, FMI Uni-Stuttgart - -16.10.06 llncs.dem 2.3 removed affiliations from \tocauthor demo - -11.12.07 llncs.doc note on online visibility of given e-mail address - -15.06.09 splncs03.bst new BibTeX style compliant with the current - requirements, provided by Maurizio "Titto" - Patrignani of Universita' Roma Tre - -30.03.10 llncs.cls 2.15 fixed broken hyperref interoperability; - patch provided by Sven Koehler, - Hamburg University of Technology - -15.04.10 llncs.cls 2.16 fixed hyperref warning for informatory TOC entries; - introduced \keywords command - finally; - blank removed from \keywordname, flaw reported - by Armin B. Wagner, IGW TU Vienna - -15.04.10 llncs.cls 2.17 fixed missing switch "openright" used by \backmatter; - flaw reported by Tobias Pape, University of Potsdam - -27.09.13 llncs.cls 2.18 fixed "ngerman" incompatibility; solution provided - by Bastian Pfleging, University of Stuttgart - -31.03.14 llncs.cls 2.19 removed spurious blanks from "babel" texts, - problem reported by Piotr Stera, Silesian University - of Technology, Gliwice, Poland - diff --git a/intro.tex b/intro.tex index c293088..5a8b663 100644 --- a/intro.tex +++ b/intro.tex @@ -1,2 +1,2 @@ \section{Introduction} -UNFINISHED \ No newline at end of file +In this paper, we develop the foundational theory used in the Lean theorem prover. diff --git a/llncs.cls b/llncs.cls deleted file mode 100644 index 6074546..0000000 --- a/llncs.cls +++ /dev/null @@ -1,1208 +0,0 @@ -% LLNCS DOCUMENT CLASS -- version 2.20 (24-JUN-2015) -% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science -% -%% -%% \CharacterTable -%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z -%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z -%% Digits \0\1\2\3\4\5\6\7\8\9 -%% Exclamation \! Double quote \" Hash (number) \# -%% Dollar \$ Percent \% Ampersand \& -%% Acute accent \' Left paren \( Right paren \) -%% Asterisk \* Plus \+ Comma \, -%% Minus \- Point \. Solidus \/ -%% Colon \: Semicolon \; Less than \< -%% Equals \= Greater than \> Question mark \? -%% Commercial at \@ Left bracket \[ Backslash \\ -%% Right bracket \] Circumflex \^ Underscore \_ -%% Grave accent \` Left brace \{ Vertical bar \| -%% Right brace \} Tilde \~} -%% -\NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesClass{llncs}[2015/06/24 v2.20 -^^J LaTeX document class for Lecture Notes in Computer Science] -% Options -\let\if@envcntreset\iffalse -\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue} -\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y} -\DeclareOption{oribibl}{\let\oribibl=Y} -\let\if@custvec\iftrue -\DeclareOption{orivec}{\let\if@custvec\iffalse} -\let\if@envcntsame\iffalse -\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue} -\let\if@envcntsect\iffalse -\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue} -\let\if@runhead\iffalse -\DeclareOption{runningheads}{\let\if@runhead\iftrue} - -\let\if@openright\iftrue -\let\if@openbib\iffalse -\DeclareOption{openbib}{\let\if@openbib\iftrue} - -% languages -\let\switcht@@therlang\relax -\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}} -\def\ds@francais{\def\switcht@@therlang{\switcht@francais}} - -\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}} - -\ProcessOptions - -\LoadClass[twoside]{article} -\RequirePackage{multicol} % needed for the list of participants, index -\RequirePackage{aliascnt} - -\setlength{\textwidth}{12.2cm} -\setlength{\textheight}{19.3cm} -\renewcommand\@pnumwidth{2em} -\renewcommand\@tocrmarg{3.5em} -% -\def\@dottedtocline#1#2#3#4#5{% - \ifnum #1>\c@tocdepth \else - \vskip \z@ \@plus.2\p@ - {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm - \parfillskip -\rightskip \pretolerance=10000 - \parindent #2\relax\@afterindenttrue - \interlinepenalty\@M - \leavevmode - \@tempdima #3\relax - \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip - {#4}\nobreak - \leaders\hbox{$\m@th - \mkern \@dotsep mu\hbox{.}\mkern \@dotsep - mu$}\hfill - \nobreak - \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}% - \par}% - \fi} -% -\def\switcht@albion{% -\def\abstractname{Abstract.}% -\def\ackname{Acknowledgement.}% -\def\andname{and}% -\def\lastandname{\unskip, and}% -\def\appendixname{Appendix}% -\def\chaptername{Chapter}% -\def\claimname{Claim}% -\def\conjecturename{Conjecture}% -\def\contentsname{Table of Contents}% -\def\corollaryname{Corollary}% -\def\definitionname{Definition}% -\def\examplename{Example}% -\def\exercisename{Exercise}% -\def\figurename{Fig.}% -\def\keywordname{{\bf Keywords:}}% -\def\indexname{Index}% -\def\lemmaname{Lemma}% -\def\contriblistname{List of Contributors}% -\def\listfigurename{List of Figures}% -\def\listtablename{List of Tables}% -\def\mailname{{\it Correspondence to\/}:}% -\def\noteaddname{Note added in proof}% -\def\notename{Note}% -\def\partname{Part}% -\def\problemname{Problem}% -\def\proofname{Proof}% -\def\propertyname{Property}% -\def\propositionname{Proposition}% -\def\questionname{Question}% -\def\remarkname{Remark}% -\def\seename{see}% -\def\solutionname{Solution}% -\def\subclassname{{\it Subject Classifications\/}:}% -\def\tablename{Table}% -\def\theoremname{Theorem}} -\switcht@albion -% Names of theorem like environments are already defined -% but must be translated if another language is chosen -% -% French section -\def\switcht@francais{%\typeout{On parle francais.}% - \def\abstractname{R\'esum\'e.}% - \def\ackname{Remerciements.}% - \def\andname{et}% - \def\lastandname{ et}% - \def\appendixname{Appendice}% - \def\chaptername{Chapitre}% - \def\claimname{Pr\'etention}% - \def\conjecturename{Hypoth\`ese}% - \def\contentsname{Table des mati\`eres}% - \def\corollaryname{Corollaire}% - \def\definitionname{D\'efinition}% - \def\examplename{Exemple}% - \def\exercisename{Exercice}% - \def\figurename{Fig.}% - \def\keywordname{{\bf Mots-cl\'e:}}% - \def\indexname{Index}% - \def\lemmaname{Lemme}% - \def\contriblistname{Liste des contributeurs}% - \def\listfigurename{Liste des figures}% - \def\listtablename{Liste des tables}% - \def\mailname{{\it Correspondence to\/}:}% - \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}% - \def\notename{Remarque}% - \def\partname{Partie}% - \def\problemname{Probl\`eme}% - \def\proofname{Preuve}% - \def\propertyname{Caract\'eristique}% -%\def\propositionname{Proposition}% - \def\questionname{Question}% - \def\remarkname{Remarque}% - \def\seename{voir}% - \def\solutionname{Solution}% - \def\subclassname{{\it Subject Classifications\/}:}% - \def\tablename{Tableau}% - \def\theoremname{Th\'eor\`eme}% -} -% -% German section -\def\switcht@deutsch{%\typeout{Man spricht deutsch.}% - \def\abstractname{Zusammenfassung.}% - \def\ackname{Danksagung.}% - \def\andname{und}% - \def\lastandname{ und}% - \def\appendixname{Anhang}% - \def\chaptername{Kapitel}% - \def\claimname{Behauptung}% - \def\conjecturename{Hypothese}% - \def\contentsname{Inhaltsverzeichnis}% - \def\corollaryname{Korollar}% -%\def\definitionname{Definition}% - \def\examplename{Beispiel}% - \def\exercisename{\"Ubung}% - \def\figurename{Abb.}% - \def\keywordname{{\bf Schl\"usselw\"orter:}}% - \def\indexname{Index}% -%\def\lemmaname{Lemma}% - \def\contriblistname{Mitarbeiter}% - \def\listfigurename{Abbildungsverzeichnis}% - \def\listtablename{Tabellenverzeichnis}% - \def\mailname{{\it Correspondence to\/}:}% - \def\noteaddname{Nachtrag}% - \def\notename{Anmerkung}% - \def\partname{Teil}% -%\def\problemname{Problem}% - \def\proofname{Beweis}% - \def\propertyname{Eigenschaft}% -%\def\propositionname{Proposition}% - \def\questionname{Frage}% - \def\remarkname{Anmerkung}% - \def\seename{siehe}% - \def\solutionname{L\"osung}% - \def\subclassname{{\it Subject Classifications\/}:}% - \def\tablename{Tabelle}% -%\def\theoremname{Theorem}% -} - -% Ragged bottom for the actual page -\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil -\global\let\@textbottom\relax}} - -\renewcommand\small{% - \@setfontsize\small\@ixpt{11}% - \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@ - \abovedisplayshortskip \z@ \@plus2\p@ - \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@ - \def\@listi{\leftmargin\leftmargini - \parsep 0\p@ \@plus1\p@ \@minus\p@ - \topsep 8\p@ \@plus2\p@ \@minus4\p@ - \itemsep0\p@}% - \belowdisplayskip \abovedisplayskip -} - -\frenchspacing -\widowpenalty=10000 -\clubpenalty=10000 - -\setlength\oddsidemargin {63\p@} -\setlength\evensidemargin {63\p@} -\setlength\marginparwidth {90\p@} - -\setlength\headsep {16\p@} - -\setlength\footnotesep{7.7\p@} -\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@} -\setlength\intextsep {8mm\@plus 2\p@ \@minus 2\p@} - -\setcounter{secnumdepth}{2} - -\newcounter {chapter} -\renewcommand\thechapter {\@arabic\c@chapter} - -\newif\if@mainmatter \@mainmattertrue -\newcommand\frontmatter{\cleardoublepage - \@mainmatterfalse\pagenumbering{Roman}} -\newcommand\mainmatter{\cleardoublepage - \@mainmattertrue\pagenumbering{arabic}} -\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi - \@mainmatterfalse} - -\renewcommand\part{\cleardoublepage - \thispagestyle{empty}% - \if@twocolumn - \onecolumn - \@tempswatrue - \else - \@tempswafalse - \fi - \null\vfil - \secdef\@part\@spart} - -\def\@part[#1]#2{% - \ifnum \c@secnumdepth >-2\relax - \refstepcounter{part}% - \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}% - \else - \addcontentsline{toc}{part}{#1}% - \fi - \markboth{}{}% - {\centering - \interlinepenalty \@M - \normalfont - \ifnum \c@secnumdepth >-2\relax - \huge\bfseries \partname~\thepart - \par - \vskip 20\p@ - \fi - \Huge \bfseries #2\par}% - \@endpart} -\def\@spart#1{% - {\centering - \interlinepenalty \@M - \normalfont - \Huge \bfseries #1\par}% - \@endpart} -\def\@endpart{\vfil\newpage - \if@twoside - \null - \thispagestyle{empty}% - \newpage - \fi - \if@tempswa - \twocolumn - \fi} - -\newcommand\chapter{\clearpage - \thispagestyle{empty}% - \global\@topnum\z@ - \@afterindentfalse - \secdef\@chapter\@schapter} -\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne - \if@mainmatter - \refstepcounter{chapter}% - \typeout{\@chapapp\space\thechapter.}% - \addcontentsline{toc}{chapter}% - {\protect\numberline{\thechapter}#1}% - \else - \addcontentsline{toc}{chapter}{#1}% - \fi - \else - \addcontentsline{toc}{chapter}{#1}% - \fi - \chaptermark{#1}% - \addtocontents{lof}{\protect\addvspace{10\p@}}% - \addtocontents{lot}{\protect\addvspace{10\p@}}% - \if@twocolumn - \@topnewpage[\@makechapterhead{#2}]% - \else - \@makechapterhead{#2}% - \@afterheading - \fi} -\def\@makechapterhead#1{% -% \vspace*{50\p@}% - {\centering - \ifnum \c@secnumdepth >\m@ne - \if@mainmatter - \large\bfseries \@chapapp{} \thechapter - \par\nobreak - \vskip 20\p@ - \fi - \fi - \interlinepenalty\@M - \Large \bfseries #1\par\nobreak - \vskip 40\p@ - }} -\def\@schapter#1{\if@twocolumn - \@topnewpage[\@makeschapterhead{#1}]% - \else - \@makeschapterhead{#1}% - \@afterheading - \fi} -\def\@makeschapterhead#1{% -% \vspace*{50\p@}% - {\centering - \normalfont - \interlinepenalty\@M - \Large \bfseries #1\par\nobreak - \vskip 40\p@ - }} - -\renewcommand\section{\@startsection{section}{1}{\z@}% - {-18\p@ \@plus -4\p@ \@minus -4\p@}% - {12\p@ \@plus 4\p@ \@minus 4\p@}% - {\normalfont\large\bfseries\boldmath - \rightskip=\z@ \@plus 8em\pretolerance=10000 }} -\renewcommand\subsection{\@startsection{subsection}{2}{\z@}% - {-18\p@ \@plus -4\p@ \@minus -4\p@}% - {8\p@ \@plus 4\p@ \@minus 4\p@}% - {\normalfont\normalsize\bfseries\boldmath - \rightskip=\z@ \@plus 8em\pretolerance=10000 }} -\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}% - {-18\p@ \@plus -4\p@ \@minus -4\p@}% - {-0.5em \@plus -0.22em \@minus -0.1em}% - {\normalfont\normalsize\bfseries\boldmath}} -\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}% - {-12\p@ \@plus -4\p@ \@minus -4\p@}% - {-0.5em \@plus -0.22em \@minus -0.1em}% - {\normalfont\normalsize\itshape}} -\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use - \string\subparagraph\space with this class}\vskip0.5cm -You should not use \verb|\subparagraph| with this class.\vskip0.5cm} - -\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00} -\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01} -\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02} -\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03} -\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04} -\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05} -\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06} -\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07} -\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08} -\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09} -\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A} - -\let\footnotesize\small - -\if@custvec -\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}} -{\mbox{\boldmath$\textstyle#1$}} -{\mbox{\boldmath$\scriptstyle#1$}} -{\mbox{\boldmath$\scriptscriptstyle#1$}}} -\fi - -\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}} -\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil -\penalty50\hskip1em\null\nobreak\hfil\squareforqed -\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi} - -\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip -\halign{\hfil -$\displaystyle##$\hfil\cr\gets\cr\to\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets -\cr\to\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets -\cr\to\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr -\gets\cr\to\cr}}}}} -\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil -$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr -\noalign{\vskip1.2pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr -\noalign{\vskip1pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr -<\cr -\noalign{\vskip0.9pt}=\cr}}}}} -\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil -$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr -\noalign{\vskip1.2pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr -\noalign{\vskip1pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr ->\cr -\noalign{\vskip0.9pt}=\cr}}}}} -\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip -\halign{\hfil -$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr ->\cr\noalign{\vskip-1pt}<\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr ->\cr\noalign{\vskip-0.8pt}<\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr ->\cr\noalign{\vskip-0.3pt}<\cr}}}}} -\def\bbbr{{\rm I\!R}} %reelle Zahlen -\def\bbbm{{\rm I\!M}} -\def\bbbn{{\rm I\!N}} %natuerliche Zahlen -\def\bbbf{{\rm I\!F}} -\def\bbbh{{\rm I\!H}} -\def\bbbk{{\rm I\!K}} -\def\bbbp{{\rm I\!P}} -\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l} -{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}} -\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox -to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox -to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox -to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox -to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}} -\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm -Q$}\hbox{\raise -0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}} -{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise -0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise -0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise -0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}} -\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm -T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox -to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox -to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox -to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}} -\def\bbbs{{\mathchoice -{\setbox0=\hbox{$\displaystyle \rm S$}\hbox{\raise0.5\ht0\hbox -to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox -to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}} -{\setbox0=\hbox{$\textstyle \rm S$}\hbox{\raise0.5\ht0\hbox -to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox -to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptstyle \rm S$}\hbox{\raise0.5\ht0\hbox -to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox -to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox -to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox -to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}} -\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}} -{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}} -{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}} -{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}} - -\let\ts\, - -\setlength\leftmargini {17\p@} -\setlength\leftmargin {\leftmargini} -\setlength\leftmarginii {\leftmargini} -\setlength\leftmarginiii {\leftmargini} -\setlength\leftmarginiv {\leftmargini} -\setlength \labelsep {.5em} -\setlength \labelwidth{\leftmargini} -\addtolength\labelwidth{-\labelsep} - -\def\@listI{\leftmargin\leftmargini - \parsep 0\p@ \@plus1\p@ \@minus\p@ - \topsep 8\p@ \@plus2\p@ \@minus4\p@ - \itemsep0\p@} -\let\@listi\@listI -\@listi -\def\@listii {\leftmargin\leftmarginii - \labelwidth\leftmarginii - \advance\labelwidth-\labelsep - \topsep 0\p@ \@plus2\p@ \@minus\p@} -\def\@listiii{\leftmargin\leftmarginiii - \labelwidth\leftmarginiii - \advance\labelwidth-\labelsep - \topsep 0\p@ \@plus\p@\@minus\p@ - \parsep \z@ - \partopsep \p@ \@plus\z@ \@minus\p@} - -\renewcommand\labelitemi{\normalfont\bfseries --} -\renewcommand\labelitemii{$\m@th\bullet$} - -\setlength\arraycolsep{1.4\p@} -\setlength\tabcolsep{1.4\p@} - -\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}% - {{\contentsname}}} - \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}} - \def\lastand{\ifnum\value{auco}=2\relax - \unskip{} \andname\ - \else - \unskip \lastandname\ - \fi}% - \def\and{\stepcounter{@auth}\relax - \ifnum\value{@auth}=\value{auco}% - \lastand - \else - \unskip, - \fi}% - \@starttoc{toc}\if@restonecol\twocolumn\fi} - -\def\l@part#1#2{\addpenalty{\@secpenalty}% - \addvspace{2em plus\p@}% % space above part line - \begingroup - \parindent \z@ - \rightskip \z@ plus 5em - \hrule\vskip5pt - \large % same size as for a contribution heading - \bfseries\boldmath % set line in boldface - \leavevmode % TeX command to enter horizontal mode. - #1\par - \vskip5pt - \hrule - \vskip1pt - \nobreak % Never break after part entry - \endgroup} - -\def\@dotsep{2} - -\let\phantomsection=\relax - -\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else -{}\fi} - -\def\addnumcontentsmark#1#2#3{% -\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline - {\thechapter}#3}{\thepage}\hyperhrefextend}}% -\def\addcontentsmark#1#2#3{% -\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}% -\def\addcontentsmarkwop#1#2#3{% -\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}% - -\def\@adcmk[#1]{\ifcase #1 \or -\def\@gtempa{\addnumcontentsmark}% - \or \def\@gtempa{\addcontentsmark}% - \or \def\@gtempa{\addcontentsmarkwop}% - \fi\@gtempa{toc}{chapter}% -} -\def\addtocmark{% -\phantomsection -\@ifnextchar[{\@adcmk}{\@adcmk[3]}% -} - -\def\l@chapter#1#2{\addpenalty{-\@highpenalty} - \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup - \parindent \z@ \rightskip \@tocrmarg - \advance\rightskip by 0pt plus 2cm - \parfillskip -\rightskip \pretolerance=10000 - \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip - {\large\bfseries\boldmath#1}\ifx0#2\hfil\null - \else - \nobreak - \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern - \@dotsep mu$}\hfill - \nobreak\hbox to\@pnumwidth{\hss #2}% - \fi\par - \penalty\@highpenalty \endgroup} - -\def\l@title#1#2{\addpenalty{-\@highpenalty} - \addvspace{8pt plus 1pt} - \@tempdima \z@ - \begingroup - \parindent \z@ \rightskip \@tocrmarg - \advance\rightskip by 0pt plus 2cm - \parfillskip -\rightskip \pretolerance=10000 - \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip - #1\nobreak - \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern - \@dotsep mu$}\hfill - \nobreak\hbox to\@pnumwidth{\hss #2}\par - \penalty\@highpenalty \endgroup} - -\def\l@author#1#2{\addpenalty{\@highpenalty} - \@tempdima=15\p@ %\z@ - \begingroup - \parindent \z@ \rightskip \@tocrmarg - \advance\rightskip by 0pt plus 2cm - \pretolerance=10000 - \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip - \textit{#1}\par - \penalty\@highpenalty \endgroup} - -\setcounter{tocdepth}{0} -\newdimen\tocchpnum -\newdimen\tocsecnum -\newdimen\tocsectotal -\newdimen\tocsubsecnum -\newdimen\tocsubsectotal -\newdimen\tocsubsubsecnum -\newdimen\tocsubsubsectotal -\newdimen\tocparanum -\newdimen\tocparatotal -\newdimen\tocsubparanum -\tocchpnum=\z@ % no chapter numbers -\tocsecnum=15\p@ % section 88. plus 2.222pt -\tocsubsecnum=23\p@ % subsection 88.8 plus 2.222pt -\tocsubsubsecnum=27\p@ % subsubsection 88.8.8 plus 1.444pt -\tocparanum=35\p@ % paragraph 88.8.8.8 plus 1.666pt -\tocsubparanum=43\p@ % subparagraph 88.8.8.8.8 plus 1.888pt -\def\calctocindent{% -\tocsectotal=\tocchpnum -\advance\tocsectotal by\tocsecnum -\tocsubsectotal=\tocsectotal -\advance\tocsubsectotal by\tocsubsecnum -\tocsubsubsectotal=\tocsubsectotal -\advance\tocsubsubsectotal by\tocsubsubsecnum -\tocparatotal=\tocsubsubsectotal -\advance\tocparatotal by\tocparanum} -\calctocindent - -\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}} -\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}} -\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}} -\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}} -\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}} - -\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn - \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}} - \@starttoc{lof}\if@restonecol\twocolumn\fi} -\def\l@figure{\@dottedtocline{1}{0em}{1.5em}} - -\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn - \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}} - \@starttoc{lot}\if@restonecol\twocolumn\fi} -\let\l@table\l@figure - -\renewcommand\listoffigures{% - \section*{\listfigurename - \@mkboth{\listfigurename}{\listfigurename}}% - \@starttoc{lof}% - } - -\renewcommand\listoftables{% - \section*{\listtablename - \@mkboth{\listtablename}{\listtablename}}% - \@starttoc{lot}% - } - -\ifx\oribibl\undefined -\ifx\citeauthoryear\undefined -\renewenvironment{thebibliography}[1] - {\section*{\refname} - \def\@biblabel##1{##1.} - \small - \list{\@biblabel{\@arabic\c@enumiv}}% - {\settowidth\labelwidth{\@biblabel{#1}}% - \leftmargin\labelwidth - \advance\leftmargin\labelsep - \if@openbib - \advance\leftmargin\bibindent - \itemindent -\bibindent - \listparindent \itemindent - \parsep \z@ - \fi - \usecounter{enumiv}% - \let\p@enumiv\@empty - \renewcommand\theenumiv{\@arabic\c@enumiv}}% - \if@openbib - \renewcommand\newblock{\par}% - \else - \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}% - \fi - \sloppy\clubpenalty4000\widowpenalty4000% - \sfcode`\.=\@m} - {\def\@noitemerr - {\@latex@warning{Empty `thebibliography' environment}}% - \endlist} -\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw - {\let\protect\noexpand\immediate - \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces} -\newcount\@tempcntc -\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi - \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do - {\@ifundefined - {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries - ?}\@warning - {Citation `\@citeb' on page \thepage \space undefined}}% - {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}% - \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne - \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}% - \else - \advance\@tempcntb\@ne - \ifnum\@tempcntb=\@tempcntc - \else\advance\@tempcntb\m@ne\@citeo - \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}} -\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else - \@citea\def\@citea{,\,\hskip\z@skip}% - \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else - {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else - \def\@citea{--}\fi - \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi} -\else -\renewenvironment{thebibliography}[1] - {\section*{\refname} - \small - \list{}% - {\settowidth\labelwidth{}% - \leftmargin\parindent - \itemindent=-\parindent - \labelsep=\z@ - \if@openbib - \advance\leftmargin\bibindent - \itemindent -\bibindent - \listparindent \itemindent - \parsep \z@ - \fi - \usecounter{enumiv}% - \let\p@enumiv\@empty - \renewcommand\theenumiv{}}% - \if@openbib - \renewcommand\newblock{\par}% - \else - \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}% - \fi - \sloppy\clubpenalty4000\widowpenalty4000% - \sfcode`\.=\@m} - {\def\@noitemerr - {\@latex@warning{Empty `thebibliography' environment}}% - \endlist} - \def\@cite#1{#1}% - \def\@lbibitem[#1]#2{\item[]\if@filesw - {\def\protect##1{\string ##1\space}\immediate - \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces} - \fi -\else -\@cons\@openbib@code{\noexpand\small} -\fi - -\def\idxquad{\hskip 10\p@}% space that divides entry from number - -\def\@idxitem{\par\hangindent 10\p@} - -\def\subitem{\par\setbox0=\hbox{--\enspace}% second order - \noindent\hangindent\wd0\box0}% index entry - -\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third - \noindent\hangindent\wd0\box0}% order index entry - -\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax} - -\renewenvironment{theindex} - {\@mkboth{\indexname}{\indexname}% - \thispagestyle{empty}\parindent\z@ - \parskip\z@ \@plus .3\p@\relax - \let\item\par - \def\,{\relax\ifmmode\mskip\thinmuskip - \else\hskip0.2em\ignorespaces\fi}% - \normalfont\small - \begin{multicols}{2}[\@makeschapterhead{\indexname}]% - } - {\end{multicols}} - -\renewcommand\footnoterule{% - \kern-3\p@ - \hrule\@width 2truecm - \kern2.6\p@} - \newdimen\fnindent - \fnindent1em -\long\def\@makefntext#1{% - \parindent \fnindent% - \leftskip \fnindent% - \noindent - \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1} - -\long\def\@makecaption#1#2{% - \small - \vskip\abovecaptionskip - \sbox\@tempboxa{{\bfseries #1.} #2}% - \ifdim \wd\@tempboxa >\hsize - {\bfseries #1.} #2\par - \else - \global \@minipagefalse - \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}% - \fi - \vskip\belowcaptionskip} - -\def\fps@figure{htbp} -\def\fnum@figure{\figurename\thinspace\thefigure} -\def \@floatboxreset {% - \reset@font - \small - \@setnobreak - \@setminipage -} -\def\fps@table{htbp} -\def\fnum@table{\tablename~\thetable} -\renewenvironment{table} - {\setlength\abovecaptionskip{0\p@}% - \setlength\belowcaptionskip{10\p@}% - \@float{table}} - {\end@float} -\renewenvironment{table*} - {\setlength\abovecaptionskip{0\p@}% - \setlength\belowcaptionskip{10\p@}% - \@dblfloat{table}} - {\end@dblfloat} - -\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname - ext@#1\endcsname}{#1}{\protect\numberline{\csname - the#1\endcsname}{\ignorespaces #2}}\begingroup - \@parboxrestore - \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par - \endgroup} - -% LaTeX does not provide a command to enter the authors institute -% addresses. The \institute command is defined here. - -\newcounter{@inst} -\newcounter{@auth} -\newcounter{auco} -\newdimen\instindent -\newbox\authrun -\newtoks\authorrunning -\newtoks\tocauthor -\newbox\titrun -\newtoks\titlerunning -\newtoks\toctitle - -\def\clearheadinfo{\gdef\@author{No Author Given}% - \gdef\@title{No Title Given}% - \gdef\@subtitle{}% - \gdef\@institute{No Institute Given}% - \gdef\@thanks{}% - \global\titlerunning={}\global\authorrunning={}% - \global\toctitle={}\global\tocauthor={}} - -\def\institute#1{\gdef\@institute{#1}} - -\def\institutename{\par - \begingroup - \parskip=\z@ - \parindent=\z@ - \setcounter{@inst}{1}% - \def\and{\par\stepcounter{@inst}% - \noindent$^{\the@inst}$\enspace\ignorespaces}% - \setbox0=\vbox{\def\thanks##1{}\@institute}% - \ifnum\c@@inst=1\relax - \gdef\fnnstart{0}% - \else - \xdef\fnnstart{\c@@inst}% - \setcounter{@inst}{1}% - \noindent$^{\the@inst}$\enspace - \fi - \ignorespaces - \@institute\par - \endgroup} - -\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or - {\star\star\star}\or \dagger\or \ddagger\or - \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger - \or \ddagger\ddagger \else\@ctrerr\fi}} - -\def\inst#1{\unskip$^{#1}$} -\def\fnmsep{\unskip$^,$} -\def\email#1{{\tt#1}} -\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}% -\@ifpackageloaded{babel}{% -\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}% -\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}% -\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}% -\@ifundefined{extrasngerman}{}{\addto\extrasngerman{\switcht@deutsch}}% -}{\switcht@@therlang}% -\providecommand{\keywords}[1]{\par\addvspace\baselineskip -\noindent\keywordname\enspace\ignorespaces#1}% -} -\def\homedir{\~{ }} - -\def\subtitle#1{\gdef\@subtitle{#1}} -\clearheadinfo -% -%%% to avoid hyperref warnings -\providecommand*{\toclevel@author}{999} -%%% to make title-entry parent of section-entries -\providecommand*{\toclevel@title}{0} -% -\renewcommand\maketitle{\newpage -\phantomsection - \refstepcounter{chapter}% - \stepcounter{section}% - \setcounter{section}{0}% - \setcounter{subsection}{0}% - \setcounter{figure}{0} - \setcounter{table}{0} - \setcounter{equation}{0} - \setcounter{footnote}{0}% - \begingroup - \parindent=\z@ - \renewcommand\thefootnote{\@fnsymbol\c@footnote}% - \if@twocolumn - \ifnum \col@number=\@ne - \@maketitle - \else - \twocolumn[\@maketitle]% - \fi - \else - \newpage - \global\@topnum\z@ % Prevents figures from going at top of page. - \@maketitle - \fi - \thispagestyle{empty}\@thanks -% - \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}% - \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}% - \instindent=\hsize - \advance\instindent by-\headlineindent - \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else - \addcontentsline{toc}{title}{\the\toctitle}\fi - \if@runhead - \if!\the\titlerunning!\else - \edef\@title{\the\titlerunning}% - \fi - \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}% - \ifdim\wd\titrun>\instindent - \typeout{Title too long for running head. Please supply}% - \typeout{a shorter form with \string\titlerunning\space prior to - \string\maketitle}% - \global\setbox\titrun=\hbox{\small\rm - Title Suppressed Due to Excessive Length}% - \fi - \xdef\@title{\copy\titrun}% - \fi -% - \if!\the\tocauthor!\relax - {\def\and{\noexpand\protect\noexpand\and}% - \protected@xdef\toc@uthor{\@author}}% - \else - \def\\{\noexpand\protect\noexpand\newline}% - \protected@xdef\scratch{\the\tocauthor}% - \protected@xdef\toc@uthor{\scratch}% - \fi - \addtocontents{toc}{\noexpand\protect\noexpand\authcount{\the\c@auco}}% - \addcontentsline{toc}{author}{\toc@uthor}% - \if@runhead - \if!\the\authorrunning! - \value{@inst}=\value{@auth}% - \setcounter{@auth}{1}% - \else - \edef\@author{\the\authorrunning}% - \fi - \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}% - \ifdim\wd\authrun>\instindent - \typeout{Names of authors too long for running head. Please supply}% - \typeout{a shorter form with \string\authorrunning\space prior to - \string\maketitle}% - \global\setbox\authrun=\hbox{\small\rm - Authors Suppressed Due to Excessive Length}% - \fi - \xdef\@author{\copy\authrun}% - \markboth{\@author}{\@title}% - \fi - \endgroup - \setcounter{footnote}{\fnnstart}% - \clearheadinfo} -% -\def\@maketitle{\newpage - \markboth{}{}% - \def\lastand{\ifnum\value{@inst}=2\relax - \unskip{} \andname\ - \else - \unskip \lastandname\ - \fi}% - \def\and{\stepcounter{@auth}\relax - \ifnum\value{@auth}=\value{@inst}% - \lastand - \else - \unskip, - \fi}% - \begin{center}% - \let\newline\\ - {\Large \bfseries\boldmath - \pretolerance=10000 - \@title \par}\vskip .8cm -\if!\@subtitle!\else {\large \bfseries\boldmath - \vskip -.65cm - \pretolerance=10000 - \@subtitle \par}\vskip .8cm\fi - \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}% - \def\thanks##1{}\@author}% - \global\value{@inst}=\value{@auth}% - \global\value{auco}=\value{@auth}% - \setcounter{@auth}{1}% -{\lineskip .5em -\noindent\ignorespaces -\@author\vskip.35cm} - {\small\institutename} - \end{center}% - } - -% definition of the "\spnewtheorem" command. -% -% Usage: -% -% \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font} -% or \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font} -% or \spnewtheorem*{env_nam}{caption}{cap_font}{body_font} -% -% New is "cap_font" and "body_font". It stands for -% fontdefinition of the caption and the text itself. -% -% "\spnewtheorem*" gives a theorem without number. -% -% A defined spnewthoerem environment is used as described -% by Lamport. -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\def\@thmcountersep{} -\def\@thmcounterend{.} - -\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}} - -% definition of \spnewtheorem with number - -\def\@spnthm#1#2{% - \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}} -\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}} - -\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname - {\@definecounter{#1}\@addtoreset{#1}{#3}% - \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand - \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}% - \expandafter\xdef\csname #1name\endcsname{#2}% - \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}% - \global\@namedef{end#1}{\@endtheorem}}} - -\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname - {\@definecounter{#1}% - \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}% - \expandafter\xdef\csname #1name\endcsname{#2}% - \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}% - \global\@namedef{end#1}{\@endtheorem}}} - -\def\@spothm#1[#2]#3#4#5{% - \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}% - {\expandafter\@ifdefinable\csname #1\endcsname - {\newaliascnt{#1}{#2}% - \expandafter\xdef\csname #1name\endcsname{#3}% - \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}% - \global\@namedef{end#1}{\@endtheorem}}}} - -\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@ -\refstepcounter{#1}\phantomsection -\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}} - -\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}% - \ignorespaces} - -\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname - the#1\endcsname}{#5}{#3}{#4}\ignorespaces} - -\def\@spbegintheorem#1#2#3#4{\trivlist - \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4} - -\def\@spopargbegintheorem#1#2#3#4#5{\trivlist - \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5} - -% definition of \spnewtheorem* without number - -\def\@sthm#1#2{\@Ynthm{#1}{#2}} - -\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname - {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}% - \expandafter\xdef\csname #1name\endcsname{#2}% - \global\@namedef{end#1}{\@endtheorem}}} - -\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@ -\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}} - -\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces} - -\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1} - {#4}{#2}{#3}\ignorespaces} - -\def\@Begintheorem#1#2#3{#3\trivlist - \item[\hskip\labelsep{#2#1\@thmcounterend}]} - -\def\@Opargbegintheorem#1#2#3#4{#4\trivlist - \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }} - -\if@envcntsect - \def\@thmcountersep{.} - \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape} -\else - \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape} - \if@envcntreset - \@addtoreset{theorem}{section} - \else - \@addtoreset{theorem}{chapter} - \fi -\fi - -%definition of divers theorem environments -\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily} -\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily} -\if@envcntsame % alle Umgebungen wie Theorem. - \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}} -\else % alle Umgebungen mit eigenem Zaehler - \if@envcntsect % mit section numeriert - \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}} - \else % nicht mit section numeriert - \if@envcntreset - \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4} - \@addtoreset{#1}{section}} - \else - \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4} - \@addtoreset{#1}{chapter}}% - \fi - \fi -\fi -\spn@wtheorem{case}{Case}{\itshape}{\rmfamily} -\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily} -\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape} -\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape} -\spn@wtheorem{example}{Example}{\itshape}{\rmfamily} -\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily} -\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape} -\spn@wtheorem{note}{Note}{\itshape}{\rmfamily} -\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily} -\spn@wtheorem{property}{Property}{\itshape}{\rmfamily} -\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape} -\spn@wtheorem{question}{Question}{\itshape}{\rmfamily} -\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily} -\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily} - -\def\@takefromreset#1#2{% - \def\@tempa{#1}% - \let\@tempd\@elt - \def\@elt##1{% - \def\@tempb{##1}% - \ifx\@tempa\@tempb\else - \@addtoreset{##1}{#2}% - \fi}% - \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname - \expandafter\def\csname cl@#2\endcsname{}% - \@tempc - \let\@elt\@tempd} - -\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist - \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5} - \def\@Opargbegintheorem##1##2##3##4{##4\trivlist - \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }} - } - -\renewenvironment{abstract}{% - \list{}{\advance\topsep by0.35cm\relax\small - \leftmargin=1cm - \labelwidth=\z@ - \listparindent=\z@ - \itemindent\listparindent - \rightmargin\leftmargin}\item[\hskip\labelsep - \bfseries\abstractname]} - {\endlist} - -\newdimen\headlineindent % dimension for space between -\headlineindent=1.166cm % number and text of headings. - -\def\ps@headings{\let\@mkboth\@gobbletwo - \let\@oddfoot\@empty\let\@evenfoot\@empty - \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}% - \leftmark\hfil} - \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}% - \llap{\thepage}} - \def\chaptermark##1{}% - \def\sectionmark##1{}% - \def\subsectionmark##1{}} - -\def\ps@titlepage{\let\@mkboth\@gobbletwo - \let\@oddfoot\@empty\let\@evenfoot\@empty - \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}% - \hfil} - \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}% - \llap{\thepage}} - \def\chaptermark##1{}% - \def\sectionmark##1{}% - \def\subsectionmark##1{}} - -\if@runhead\ps@headings\else -\ps@empty\fi - -\setlength\arraycolsep{1.4\p@} -\setlength\tabcolsep{1.4\p@} - -\endinput -%end of file llncs.cls diff --git a/llncsdoc.sty b/llncsdoc.sty deleted file mode 100644 index a349619..0000000 --- a/llncsdoc.sty +++ /dev/null @@ -1,42 +0,0 @@ -% This is LLNCSDOC.STY the modification of the -% LLNCS class file for the documentation of -% the class itself. -% -\def\AmS{{\protect\usefont{OMS}{cmsy}{m}{n}% - A\kern-.1667em\lower.5ex\hbox{M}\kern-.125emS}} -\def\AmSTeX{{\protect\AmS-\protect\TeX}} -% -\def\ps@myheadings{\let\@mkboth\@gobbletwo -\def\@oddhead{\hbox{}\hfil\small\rm\rightmark -\qquad\thepage}% -\def\@oddfoot{}\def\@evenhead{\small\rm\thepage\qquad -\leftmark\hfil}% -\def\@evenfoot{}\def\sectionmark##1{}\def\subsectionmark##1{}} -\ps@myheadings -% -\setcounter{tocdepth}{2} -% -\renewcommand{\labelitemi}{--} -\newenvironment{alpherate}% -{\renewcommand{\labelenumi}{\alph{enumi})}\begin{enumerate}}% -{\end{enumerate}\renewcommand{\labelenumi}{enumi}} -% -\def\bibauthoryear{\begingroup -\def\thebibliography##1{\section*{References}% - \small\list{}{\settowidth\labelwidth{}\leftmargin\parindent - \itemindent=-\parindent - \labelsep=\z@ - \usecounter{enumi}}% - \def\newblock{\hskip .11em plus .33em minus -.07em}% - \sloppy - \sfcode`\.=1000\relax}% - \def\@cite##1{##1}% - \def\@lbibitem[##1]##2{\item[]\if@filesw - {\def\protect####1{\string ####1\space}\immediate - \write\@auxout{\string\bibcite{##2}{##1}}}\fi\ignorespaces}% -\begin{thebibliography}{} -\bibitem[1982]{clar:eke3} Clarke, F., Ekeland, I.: Nonlinear -oscillations and boundary-value problems for Hamiltonian systems. -Arch. Rat. Mech. Anal. 78, 315--333 (1982) -\end{thebibliography} -\endgroup} diff --git a/main.out b/main.out new file mode 100644 index 0000000..121efdc --- /dev/null +++ b/main.out @@ -0,0 +1,31 @@ +\BOOKMARK [1][-]{section.1}{Introduction}{}% 1 +\BOOKMARK [1][-]{section.2}{The axioms}{}% 2 +\BOOKMARK [2][-]{subsection.2.1}{Typing}{section.2}% 3 +\BOOKMARK [2][-]{subsection.2.2}{Definitional equality}{section.2}% 4 +\BOOKMARK [2][-]{subsection.2.3}{Reduction}{section.2}% 5 +\BOOKMARK [2][-]{subsection.2.4}{let binders \( reduction\)}{section.2}% 6 +\BOOKMARK [2][-]{subsection.2.5}{Definitions \( reduction\)}{section.2}% 7 +\BOOKMARK [2][-]{subsection.2.6}{Inductive types}{section.2}% 8 +\BOOKMARK [3][-]{subsubsection.2.6.1}{Inductive specifications}{subsection.2.6}% 9 +\BOOKMARK [3][-]{subsubsection.2.6.2}{Large elimination}{subsection.2.6}% 10 +\BOOKMARK [3][-]{subsubsection.2.6.3}{The recursor}{subsection.2.6}% 11 +\BOOKMARK [3][-]{subsubsection.2.6.4}{The computation rule \( reduction\)}{subsection.2.6}% 12 +\BOOKMARK [2][-]{subsection.2.7}{Non-primitive axioms}{section.2}% 13 +\BOOKMARK [3][-]{subsubsection.2.7.1}{Quotient types}{subsection.2.7}% 14 +\BOOKMARK [3][-]{subsubsection.2.7.2}{Propositional extensionality}{subsection.2.7}% 15 +\BOOKMARK [3][-]{subsubsection.2.7.3}{Axiom of choice}{subsection.2.7}% 16 +\BOOKMARK [1][-]{section.3}{Properties of the type system}{}% 17 +\BOOKMARK [2][-]{subsection.3.1}{Undecidability of definitional equality}{section.3}% 18 +\BOOKMARK [3][-]{subsubsection.3.1.1}{Algorithmic equality is not transitive}{subsection.3.1}% 19 +\BOOKMARK [3][-]{subsubsection.3.1.2}{Failure of subject reduction}{subsection.3.1}% 20 +\BOOKMARK [2][-]{subsection.3.2}{Regularity}{section.3}% 21 +\BOOKMARK [2][-]{subsection.3.3}{Unique typing}{section.3}% 22 +\BOOKMARK [2][-]{subsection.3.4}{The Church-Rosser theorem}{section.3}% 23 +\BOOKMARK [1][-]{section.4}{Reduction of inductive types to W-types}{}% 24 +\BOOKMARK [2][-]{subsubsection.4.0.1}{Translating type families}{section.4}% 25 +\BOOKMARK [3][-]{subsubsection.4.0.2}{Translating K-like eliminators}{subsubsection.4.0.1}% 26 +\BOOKMARK [3][-]{subsubsection.4.0.3}{The remainder}{subsubsection.4.0.1}% 27 +\BOOKMARK [1][-]{section.5}{Modeling Lean in ZFC}{}% 28 +\BOOKMARK [2][-]{subsubsection.5.0.1}{Definition of W-types in ZFC}{section.5}% 29 +\BOOKMARK [3][-]{subsubsection.5.0.2}{Definition of acc in ZFC}{subsubsection.5.0.1}% 30 +\BOOKMARK [2][-]{subsection.5.1}{Soundness}{section.5}% 31 diff --git a/main.tex b/main.tex index 099a9e6..65bf95d 100644 --- a/main.tex +++ b/main.tex @@ -6,21 +6,13 @@ % See http://www.springer.com/computer/lncs/lncs+authors?SGWID=0-40209-0-0-0 % for the full guidelines. % -\documentclass{llncs} -\usepackage{amsfonts} -\usepackage[utf8x]{inputenc} -\usepackage{amsmath,amssymb,graphicx,stmaryrd} +\documentclass[11pt]{article} -\usepackage{color} -\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1} % red -\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4} % grey -\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6} % blue -\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1} % green - -\usepackage{listings} -\def\lstlanguagefiles{lstlean.tex} -\lstset{language=lean} -\lstMakeShortInline" +\usepackage[utf8]{inputenc} +\usepackage[english]{babel} +\usepackage{amsmath,amsthm,amssymb,graphicx,stmaryrd} +\usepackage[margin=1in]{geometry} +\usepackage{hyperref} \newcommand{\vph}{\varphi} \newcommand{\vep}{\varepsilon} @@ -64,39 +56,26 @@ \newcommand{\reflect@squig}[2]{\reflectbox{$\m@th#1\rightsquigarrow$}} \makeatother +\newtheorem{theorem}{Theorem} +\newtheorem{lemma}{Lemma} +\newtheorem{remark}{Remark} +\newtheorem{definition}{Definition} + +\parindent0pt \parskip10pt % make block paragraphs +\raggedright % do not right justify + \begin{document} \title{The Type Theory of Lean} -% -%\titlerunning{Matiyasevi\v{c}'s Theorem} % abbreviated title (for running head) -% also used for the TOC unless -% \toctitle is used -% \author{Mario Carneiro} -% -\authorrunning{Mario Carneiro} % abbreviated author list (for running head) -% -%%%% list of authors for the TOC (use if author list has to be modified) -% -\institute{Carnegie Mellon University, Pittsburgh PA 15289, USA,\\ -\email{mcarneir@andrew.cmu.edu}} -\maketitle % typeset the title of the contribution +\maketitle % Print title page. +\tableofcontents % Print table of contents -\begin{abstract} -In this paper, we develop the foundational theory used in the Lean theorem prover. -\keywords{Lean, Type Theory} -\end{abstract} -%\input{intro} -%\input{axioms} +\input{intro} +\input{axioms} \input{typesys} \input{Wtypes} \input{soundness} -% -% ---- Bibliography ---- -% -%\begin{thebibliography}{5} -% -%\end{thebibliography} \end{document} diff --git a/main.toc b/main.toc new file mode 100644 index 0000000..88e0fa3 --- /dev/null +++ b/main.toc @@ -0,0 +1,32 @@ +\babel@toc {english}{} +\contentsline {section}{\numberline {1}Introduction}{2}{section.1} +\contentsline {section}{\numberline {2}The axioms}{2}{section.2} +\contentsline {subsection}{\numberline {2.1}Typing}{2}{subsection.2.1} +\contentsline {subsection}{\numberline {2.2}Definitional equality}{3}{subsection.2.2} +\contentsline {subsection}{\numberline {2.3}Reduction}{4}{subsection.2.3} +\contentsline {subsection}{\numberline {2.4}\textsf {let} binders ($\zeta $ reduction)}{5}{subsection.2.4} +\contentsline {subsection}{\numberline {2.5}Definitions ($\delta $ reduction)}{5}{subsection.2.5} +\contentsline {subsection}{\numberline {2.6}Inductive types}{7}{subsection.2.6} +\contentsline {subsubsection}{\numberline {2.6.1}Inductive specifications}{7}{subsubsection.2.6.1} +\contentsline {subsubsection}{\numberline {2.6.2}Large elimination}{8}{subsubsection.2.6.2} +\contentsline {subsubsection}{\numberline {2.6.3}The recursor}{9}{subsubsection.2.6.3} +\contentsline {subsubsection}{\numberline {2.6.4}The computation rule ($\iota $ reduction)}{10}{subsubsection.2.6.4} +\contentsline {subsection}{\numberline {2.7}Non-primitive axioms}{11}{subsection.2.7} +\contentsline {subsubsection}{\numberline {2.7.1}Quotient types}{11}{subsubsection.2.7.1} +\contentsline {subsubsection}{\numberline {2.7.2}Propositional extensionality}{11}{subsubsection.2.7.2} +\contentsline {subsubsection}{\numberline {2.7.3}Axiom of choice}{12}{subsubsection.2.7.3} +\contentsline {section}{\numberline {3}Properties of the type system}{12}{section.3} +\contentsline {subsection}{\numberline {3.1}Undecidability of definitional equality}{12}{subsection.3.1} +\contentsline {subsubsection}{\numberline {3.1.1}Algorithmic equality is not transitive}{13}{subsubsection.3.1.1} +\contentsline {subsubsection}{\numberline {3.1.2}Failure of subject reduction}{14}{subsubsection.3.1.2} +\contentsline {subsection}{\numberline {3.2}Regularity}{14}{subsection.3.2} +\contentsline {subsection}{\numberline {3.3}Unique typing}{16}{subsection.3.3} +\contentsline {subsection}{\numberline {3.4}The Church-Rosser theorem}{18}{subsection.3.4} +\contentsline {section}{\numberline {4}Reduction of inductive types to $\mathsf {W}$-types}{26}{section.4} +\contentsline {subsubsection}{\numberline {4.0.1}Translating type families}{28}{subsubsection.4.0.1} +\contentsline {subsubsection}{\numberline {4.0.2}Translating K-like eliminators}{30}{subsubsection.4.0.2} +\contentsline {subsubsection}{\numberline {4.0.3}The remainder}{31}{subsubsection.4.0.3} +\contentsline {section}{\numberline {5}Modeling Lean in ZFC}{32}{section.5} +\contentsline {subsubsection}{\numberline {5.0.1}Definition of $\mathsf {W}$-types in ZFC}{35}{subsubsection.5.0.1} +\contentsline {subsubsection}{\numberline {5.0.2}Definition of $\mathsf {acc}$ in ZFC}{35}{subsubsection.5.0.2} +\contentsline {subsection}{\numberline {5.1}Soundness}{35}{subsection.5.1} diff --git a/readme.txt b/readme.txt deleted file mode 100644 index e00cde5..0000000 --- a/readme.txt +++ /dev/null @@ -1,30 +0,0 @@ -Dear LLNCS user, - -The files in this directory belong to the LaTeX2e package for -Lecture Notes in Computer Science (LNCS) of Springer-Verlag. - -It consists of the following files: - - readme.txt this file - - history.txt the version history of the package - - llncs.cls the LaTeX2e document class - - llncs.dem the sample input file - - llncs.doc the documentation of the class (LaTeX source) - llncsdoc.pdf the documentation of the class (PDF version) - llncsdoc.sty the modification of the class for the documentation - llncs.ind an external (faked) author index file - subjidx.ind subject index demo from the Springer book package - llncs.dvi the resultig DVI file (remember to use binary transfer!) - - sprmindx.sty supplementary style file for MakeIndex - (usage: makeindex -s sprmindx.sty ) - - splncs03.bst current LNCS BibTeX style with alphabetic sorting - - aliascnt.sty part of the Oberdiek bundle; allows more control over - the counters associated to any numbered item - remreset.sty by David Carlisle diff --git a/remreset.sty b/remreset.sty deleted file mode 100644 index a1e0dd8..0000000 --- a/remreset.sty +++ /dev/null @@ -1,38 +0,0 @@ -% remreset package -%%%%%%%%%%%%%%%%%% - -% Copyright 1997 David carlisle -% This file may be distributed under the terms of the LPPL. -% See 00readme.txt for details. - -% 1997/09/28 David Carlisle - -% LaTeX includes a command \@addtoreset that is used to declare that -% a counter should be reset every time a second counter is incremented. - -% For example the book class has a line -% \@addtoreset{footnote}{chapter} -% So that the footnote counter is reset each chapter. - -% If you wish to bas a new class on book, but without this counter -% being reset, then standard LaTeX gives no simple mechanism to do -% this. - -% This package defines |\@removefromreset| which just undoes the effect -% of \@addtorest. So for example a class file may be defined by - -% \LoadClass{book} -% \@removefromreset{footnote}{chapter} - - -\def\@removefromreset#1#2{{% - \expandafter\let\csname c@#1\endcsname\@removefromreset - \def\@elt##1{% - \expandafter\ifx\csname c@##1\endcsname\@removefromreset - \else - \noexpand\@elt{##1}% - \fi}% - \expandafter\xdef\csname cl@#2\endcsname{% - \csname cl@#2\endcsname}}} - - diff --git a/splncs.bst b/splncs.bst deleted file mode 100644 index 06e0e2f..0000000 --- a/splncs.bst +++ /dev/null @@ -1,1095 +0,0 @@ -% BibTeX bibliography style `splncs' - -% An attempt to match the bibliography style required for use with -% numbered references in Springer Verlag's "Lecture Notes in Computer -% Science" series. (See Springer's documentation for llncs.sty for -% more details of the suggested reference format.) Note that this -% file will not work for author-year style citations. - -% Use \documentclass{llncs} and \bibliographystyle{splncs}, and cite -% a reference with (e.g.) \cite{smith77} to get a "[1]" in the text. - -% Copyright (C) 1999 Jason Noble. -% Last updated: Friday 07 March 2006, 08:04:42 Frank Holzwarth, Springer -% -% Based on the BibTeX standard bibliography style `unsrt' - -ENTRY - { address - author - booktitle - chapter - edition - editor - howpublished - institution - journal - key - month - note - number - organization - pages - publisher - school - series - title - type - volume - year - } - {} - { label } - -INTEGERS { output.state before.all mid.sentence after.sentence - after.block after.authors between.elements} - -FUNCTION {init.state.consts} -{ #0 'before.all := - #1 'mid.sentence := - #2 'after.sentence := - #3 'after.block := - #4 'after.authors := - #5 'between.elements := -} - -STRINGS { s t } - -FUNCTION {output.nonnull} -{ 's := - output.state mid.sentence = - { " " * write$ } - { output.state after.block = - { add.period$ write$ - newline$ - "\newblock " write$ - } - { - output.state after.authors = - { ": " * write$ - newline$ - "\newblock " write$ - } - { output.state between.elements = - { ", " * write$ } - { output.state before.all = - 'write$ - { add.period$ " " * write$ } - if$ - } - if$ - } - if$ - } - if$ - mid.sentence 'output.state := - } - if$ - s -} - -FUNCTION {output} -{ duplicate$ empty$ - 'pop$ - 'output.nonnull - if$ -} - -FUNCTION {output.check} -{ 't := - duplicate$ empty$ - { pop$ "empty " t * " in " * cite$ * warning$ } - 'output.nonnull - if$ -} - -FUNCTION {output.bibitem} -{ newline$ - "\bibitem{" write$ - cite$ write$ - "}" write$ - newline$ - "" - before.all 'output.state := -} - -FUNCTION {fin.entry} -{ write$ - newline$ -} - -FUNCTION {new.block} -{ output.state before.all = - 'skip$ - { after.block 'output.state := } - if$ -} - -FUNCTION {stupid.colon} -{ after.authors 'output.state := } - -FUNCTION {insert.comma} -{ output.state before.all = - 'skip$ - { between.elements 'output.state := } - if$ -} - -FUNCTION {new.sentence} -{ output.state after.block = - 'skip$ - { output.state before.all = - 'skip$ - { after.sentence 'output.state := } - if$ - } - if$ -} - -FUNCTION {not} -{ { #0 } - { #1 } - if$ -} - -FUNCTION {and} -{ 'skip$ - { pop$ #0 } - if$ -} - -FUNCTION {or} -{ { pop$ #1 } - 'skip$ - if$ -} - -FUNCTION {new.block.checka} -{ empty$ - 'skip$ - 'new.block - if$ -} - -FUNCTION {new.block.checkb} -{ empty$ - swap$ empty$ - and - 'skip$ - 'new.block - if$ -} - -FUNCTION {new.sentence.checka} -{ empty$ - 'skip$ - 'new.sentence - if$ -} - -FUNCTION {new.sentence.checkb} -{ empty$ - swap$ empty$ - and - 'skip$ - 'new.sentence - if$ -} - -FUNCTION {field.or.null} -{ duplicate$ empty$ - { pop$ "" } - 'skip$ - if$ -} - -FUNCTION {emphasize} -{ duplicate$ empty$ - { pop$ "" } - { "" swap$ * "" * } - if$ -} - -FUNCTION {bold} -{ duplicate$ empty$ - { pop$ "" } - { "\textbf{" swap$ * "}" * } - if$ -} - -FUNCTION {parens} -{ duplicate$ empty$ - { pop$ "" } - { "(" swap$ * ")" * } - if$ -} - -INTEGERS { nameptr namesleft numnames } - -FUNCTION {format.springer.names} -{ 's := - #1 'nameptr := - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { s nameptr "{vv~}{ll}{, jj}{, f{.}.}" format.name$ 't := - nameptr #1 > - { namesleft #1 > - { ", " * t * } - { numnames #1 > - { ", " * } - 'skip$ - if$ - t "others" = - { " et~al." * } - { "" * t * } - if$ - } - if$ - } - 't - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ -} - -FUNCTION {format.names} -{ 's := - #1 'nameptr := - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { s nameptr "{vv~}{ll}{, jj}{, f.}" format.name$ 't := - nameptr #1 > - { namesleft #1 > - { ", " * t * } - { numnames #2 > - { "," * } - 'skip$ - if$ - t "others" = - { " et~al." * } - { " \& " * t * } - if$ - } - if$ - } - 't - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ -} - -FUNCTION {format.authors} -{ author empty$ - { "" } - { author format.springer.names } - if$ -} - -FUNCTION {format.editors} -{ editor empty$ - { "" } - { editor format.springer.names - editor num.names$ #1 > - { ", eds." * } - { ", ed." * } - if$ - } - if$ -} - -FUNCTION {format.title} -{ title empty$ - { "" } - { title "t" change.case$ } - if$ -} - -FUNCTION {n.dashify} -{ 't := - "" - { t empty$ not } - { t #1 #1 substring$ "-" = - { t #1 #2 substring$ "--" = not - { "--" * - t #2 global.max$ substring$ 't := - } - { { t #1 #1 substring$ "-" = } - { "-" * - t #2 global.max$ substring$ 't := - } - while$ - } - if$ - } - { t #1 #1 substring$ * - t #2 global.max$ substring$ 't := - } - if$ - } - while$ -} - -FUNCTION {format.date} -{ year empty$ - { month empty$ - { "" } - { "there's a month but no year in " cite$ * warning$ - month - } - if$ - } - { month empty$ - 'year - { month " " * year * } - if$ - } - if$ -} - -FUNCTION {format.btitle} -{ title emphasize -} - -FUNCTION {tie.or.space.connect} -{ duplicate$ text.length$ #3 < - { "~" } - { " " } - if$ - swap$ * * -} - -FUNCTION {either.or.check} -{ empty$ - 'pop$ - { "can't use both " swap$ * " fields in " * cite$ * warning$ } - if$ -} - -FUNCTION {format.bvolume} -{ volume empty$ - { "" } - { "Volume" volume tie.or.space.connect - series empty$ - 'skip$ - { " of " * series emphasize * } - if$ - add.period$ - "volume and number" number either.or.check - } - if$ -} - -FUNCTION {format.number.series} -{ volume empty$ - { number empty$ - { series field.or.null } - { output.state mid.sentence = - { "number" } - { "Number" } - if$ - number tie.or.space.connect - series empty$ - { "there's a number but no series in " cite$ * warning$ } - { " in " * series * } - if$ - } - if$ - } - { "" } - if$ -} - -FUNCTION {format.edition} -{ edition empty$ - { "" } - { output.state mid.sentence = - { edition "l" change.case$ " edn." * } - { edition "t" change.case$ " edn." * } - if$ - } - if$ -} - -INTEGERS { multiresult } - -FUNCTION {multi.page.check} -{ 't := - #0 'multiresult := - { multiresult not - t empty$ not - and - } - { t #1 #1 substring$ - duplicate$ "-" = - swap$ duplicate$ "," = - swap$ "+" = - or or - { #1 'multiresult := } - { t #2 global.max$ substring$ 't := } - if$ - } - while$ - multiresult -} - -FUNCTION {format.pages} -{ pages empty$ - { "" } - { pages multi.page.check - { "" pages n.dashify tie.or.space.connect } - { "" pages tie.or.space.connect } - if$ - } - if$ -} - -FUNCTION {format.vol} -{ volume bold -} - -FUNCTION {format.vol.num} -{ volume bold -number empty$ -{ } -{ number "(" swap$ * * ")" * } -if$ -} - -FUNCTION {pre.format.pages} -{ pages empty$ - 'skip$ - { duplicate$ empty$ - { pop$ format.pages } - { " " * pages n.dashify * } - if$ - } - if$ -} - -FUNCTION {format.chapter.pages} -{ chapter empty$ - 'format.pages - { type empty$ - { "chapter" } - { type "l" change.case$ } - if$ - chapter tie.or.space.connect - pages empty$ - 'skip$ - { " " * format.pages * } - if$ - } - if$ -} - -FUNCTION {format.in.ed.booktitle} -{ booktitle empty$ - { "" } - { editor empty$ - { "In: " booktitle emphasize * } - { "In " format.editors * ": " * booktitle emphasize * } - if$ - } - if$ -} - -FUNCTION {empty.misc.check} -{ author empty$ title empty$ howpublished empty$ - month empty$ year empty$ note empty$ - and and and and and - { "all relevant fields are empty in " cite$ * warning$ } - 'skip$ - if$ -} - -FUNCTION {format.thesis.type} -{ type empty$ - 'skip$ - { pop$ - type "t" change.case$ - } - if$ -} - -FUNCTION {format.tr.number} -{ type empty$ - { "Technical Report" } - 'type - if$ - number empty$ - { "t" change.case$ } - { number tie.or.space.connect } - if$ -} - -FUNCTION {format.article.crossref} -{ key empty$ - { journal empty$ - { "need key or journal for " cite$ * " to crossref " * crossref * - warning$ - "" - } - { "In {\em " journal * "\/}" * } - if$ - } - { "In " key * } - if$ - " \cite{" * crossref * "}" * -} - -FUNCTION {format.crossref.editor} -{ editor #1 "{vv~}{ll}" format.name$ - editor num.names$ duplicate$ - #2 > - { pop$ " et~al." * } - { #2 < - 'skip$ - { editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" = - { " et~al." * } - { " and " * editor #2 "{vv~}{ll}" format.name$ * } - if$ - } - if$ - } - if$ -} - -FUNCTION {format.book.crossref} -{ volume empty$ - { "empty volume in " cite$ * "'s crossref of " * crossref * warning$ - "In " - } - { "Volume" volume tie.or.space.connect - " of " * - } - if$ - " \cite{" * crossref * "}" * -} - -FUNCTION {format.incoll.inproc.crossref} -{ editor empty$ - editor field.or.null author field.or.null = - or - { key empty$ - { booktitle empty$ - { "need editor, key, or booktitle for " cite$ * " to crossref " * - crossref * warning$ - "" - } - { "" } - if$ - } - { "" } - if$ - } - { "" } - if$ - " \cite{" * crossref * "}" * -} - -FUNCTION {and.the.note} -{ note output - note empty$ - 'skip$ - { add.period$ } - if$ -} - -FUNCTION {article} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - crossref missing$ - { journal emphasize "journal" output.check - format.vol.num output - format.date parens output - format.pages output - } - { format.article.crossref output.nonnull - format.pages output - } - if$ - and.the.note - fin.entry -} - -FUNCTION {book} -{ output.bibitem - author empty$ - { format.editors "author and editor" output.check } - { format.authors output.nonnull - crossref missing$ - { "author and editor" editor either.or.check } - 'skip$ - if$ - } - if$ - stupid.colon - format.btitle "title" output.check - new.sentence - crossref missing$ - { format.edition output - format.bvolume output - new.block - format.number.series output - new.sentence - publisher "publisher" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - } - { format.book.crossref output.nonnull - } - if$ - and.the.note - fin.entry -} - -FUNCTION {booklet} -{ output.bibitem - format.authors output - stupid.colon - format.title "title" output.check - howpublished address new.block.checkb - howpublished output - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - and.the.note - fin.entry -} - -FUNCTION {inbook} -{ output.bibitem - author empty$ - { format.editors "author and editor" output.check } - { format.authors output.nonnull - crossref missing$ - { "author and editor" editor either.or.check } - 'skip$ - if$ - } - if$ - stupid.colon - crossref missing$ - { chapter output - new.block - format.number.series output - new.sentence - "In:" output - format.btitle "title" output.check - new.sentence - format.edition output - format.bvolume output - publisher "publisher" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - } - { chapter output - new.block - format.incoll.inproc.crossref output.nonnull - } - if$ - format.pages output - and.the.note - fin.entry -} - -FUNCTION {incollection} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - crossref missing$ - { format.in.ed.booktitle "booktitle" output.check - new.sentence - format.bvolume output - format.number.series output - new.block - format.edition output - publisher "publisher" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - format.pages output - } - { format.incoll.inproc.crossref output.nonnull - format.chapter.pages output - } - if$ - and.the.note - fin.entry -} - -FUNCTION {inproceedings} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - crossref missing$ - { format.in.ed.booktitle "booktitle" output.check - new.sentence - format.bvolume output - format.number.series output - address empty$ - { organization publisher new.sentence.checkb - organization empty$ - 'skip$ - { insert.comma } - if$ - organization output - publisher empty$ - 'skip$ - { insert.comma } - if$ - publisher output - format.date parens output - } - { insert.comma - address output.nonnull - organization empty$ - 'skip$ - { insert.comma } - if$ - organization output - publisher empty$ - 'skip$ - { insert.comma } - if$ - publisher output - format.date parens output - } - if$ - } - { format.incoll.inproc.crossref output.nonnull - } - if$ - format.pages output - and.the.note - fin.entry -} - -FUNCTION {conference} { inproceedings } - -FUNCTION {manual} -{ output.bibitem - author empty$ - { organization empty$ - 'skip$ - { organization output.nonnull - address output - } - if$ - } - { format.authors output.nonnull } - if$ - stupid.colon - format.btitle "title" output.check - author empty$ - { organization empty$ - { address new.block.checka - address output - } - 'skip$ - if$ - } - { organization address new.block.checkb - organization output - address empty$ - 'skip$ - { insert.comma } - if$ - address output - } - if$ - new.sentence - format.edition output - format.date parens output - and.the.note - fin.entry -} - -FUNCTION {mastersthesis} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - "Master's thesis" format.thesis.type output.nonnull - school empty$ - 'skip$ - { insert.comma } - if$ - school "school" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - and.the.note - fin.entry -} - -FUNCTION {misc} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - howpublished new.block.checka - howpublished output - format.date parens output - and.the.note - fin.entry - empty.misc.check -} - -FUNCTION {phdthesis} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.btitle "title" output.check - new.block - "PhD thesis" format.thesis.type output.nonnull - school empty$ - 'skip$ - { insert.comma } - if$ - school "school" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - and.the.note - fin.entry -} - -FUNCTION {proceedings} -{ output.bibitem - editor empty$ - { organization empty$ - { "" } - { organization output - stupid.colon } - if$ - } - { format.editors output.nonnull - stupid.colon - } - if$ - format.btitle "title" output.check - new.block - crossref missing$ - { format.in.ed.booktitle "booktitle" output.check - new.sentence - format.bvolume output - format.number.series output - address empty$ - { organization publisher new.sentence.checkb - organization empty$ - 'skip$ - { insert.comma } - if$ - organization output - publisher empty$ - 'skip$ - { insert.comma } - if$ - publisher output - format.date parens output - } - { insert.comma - address output.nonnull - organization empty$ - 'skip$ - { insert.comma } - if$ - organization output - publisher empty$ - 'skip$ - { insert.comma } - if$ - publisher output - format.date parens output - } - if$ - } - { format.incoll.inproc.crossref output.nonnull - } - if$ - and.the.note - fin.entry -} - -FUNCTION {techreport} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - format.tr.number output.nonnull - institution empty$ - 'skip$ - { insert.comma } - if$ - institution "institution" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - and.the.note - fin.entry -} - -FUNCTION {unpublished} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - note "note" output.check - format.date parens output - fin.entry -} - -FUNCTION {default.type} { misc } - -MACRO {jan} {"January"} - -MACRO {feb} {"February"} - -MACRO {mar} {"March"} - -MACRO {apr} {"April"} - -MACRO {may} {"May"} - -MACRO {jun} {"June"} - -MACRO {jul} {"July"} - -MACRO {aug} {"August"} - -MACRO {sep} {"September"} - -MACRO {oct} {"October"} - -MACRO {nov} {"November"} - -MACRO {dec} {"December"} - -MACRO {acmcs} {"ACM Computing Surveys"} - -MACRO {acta} {"Acta Informatica"} - -MACRO {cacm} {"Communications of the ACM"} - -MACRO {ibmjrd} {"IBM Journal of Research and Development"} - -MACRO {ibmsj} {"IBM Systems Journal"} - -MACRO {ieeese} {"IEEE Transactions on Software Engineering"} - -MACRO {ieeetc} {"IEEE Transactions on Computers"} - -MACRO {ieeetcad} - {"IEEE Transactions on Computer-Aided Design of Integrated Circuits"} - -MACRO {ipl} {"Information Processing Letters"} - -MACRO {jacm} {"Journal of the ACM"} - -MACRO {jcss} {"Journal of Computer and System Sciences"} - -MACRO {scp} {"Science of Computer Programming"} - -MACRO {sicomp} {"SIAM Journal on Computing"} - -MACRO {tocs} {"ACM Transactions on Computer Systems"} - -MACRO {tods} {"ACM Transactions on Database Systems"} - -MACRO {tog} {"ACM Transactions on Graphics"} - -MACRO {toms} {"ACM Transactions on Mathematical Software"} - -MACRO {toois} {"ACM Transactions on Office Information Systems"} - -MACRO {toplas} {"ACM Transactions on Programming Languages and Systems"} - -MACRO {tcs} {"Theoretical Computer Science"} - -READ - -STRINGS { longest.label } - -INTEGERS { number.label longest.label.width } - -FUNCTION {initialize.longest.label} -{ "" 'longest.label := - #1 'number.label := - #0 'longest.label.width := -} - -FUNCTION {longest.label.pass} -{ number.label int.to.str$ 'label := - number.label #1 + 'number.label := - label width$ longest.label.width > - { label 'longest.label := - label width$ 'longest.label.width := - } - 'skip$ - if$ -} - -EXECUTE {initialize.longest.label} - -ITERATE {longest.label.pass} - -FUNCTION {begin.bib} -{ preamble$ empty$ - 'skip$ - { preamble$ write$ newline$ } - if$ - "\begin{thebibliography}{" longest.label * "}" * write$ newline$ -} - -EXECUTE {begin.bib} - -EXECUTE {init.state.consts} - -ITERATE {call.type$} - -FUNCTION {end.bib} -{ newline$ - "\end{thebibliography}" write$ newline$ -} - -EXECUTE {end.bib} \ No newline at end of file diff --git a/splncs03.bst b/splncs03.bst deleted file mode 100644 index cc7c253..0000000 --- a/splncs03.bst +++ /dev/null @@ -1,1519 +0,0 @@ -%% BibTeX bibliography style `splncs03' -%% -%% BibTeX bibliography style for use with numbered references in -%% Springer Verlag's "Lecture Notes in Computer Science" series. -%% (See Springer's documentation for llncs.cls for -%% more details of the suggested reference format.) Note that this -%% file will not work for author-year style citations. -%% -%% Use \documentclass{llncs} and \bibliographystyle{splncs03}, and cite -%% a reference with (e.g.) \cite{smith77} to get a "[1]" in the text. -%% -%% This file comes to you courtesy of Maurizio "Titto" Patrignani of -%% Dipartimento di Informatica e Automazione Universita' Roma Tre -%% -%% ================================================================================================ -%% This was file `titto-lncs-02.bst' produced on Wed Apr 1, 2009 -%% Edited by hand by titto based on `titto-lncs-01.bst' (see below) -%% -%% CHANGES (with respect to titto-lncs-01.bst): -%% - Removed the call to \urlprefix (thus no "URL" string is added to the output) -%% ================================================================================================ -%% This was file `titto-lncs-01.bst' produced on Fri Aug 22, 2008 -%% Edited by hand by titto based on `titto.bst' (see below) -%% -%% CHANGES (with respect to titto.bst): -%% - Removed the "capitalize" command for editors string "(eds.)" and "(ed.)" -%% - Introduced the functions titto.bbl.pages and titto.bbl.page for journal pages (without "pp.") -%% - Added a new.sentence command to separate with a dot booktitle and series in the inproceedings -%% - Commented all new.block commands before urls and notes (to separate them with a comma) -%% - Introduced the functions titto.bbl.volume for handling journal volumes (without "vol." label) -%% - Used for editors the same name conventions used for authors (see function format.in.ed.booktitle) -%% - Removed a \newblock to avoid long spaces between title and "In: ..." -%% - Added function titto.space.prefix to add a space instead of "~" after the (removed) "vol." label -%% ================================================================================================ -%% This was file `titto.bst', -%% generated with the docstrip utility. -%% -%% The original source files were: -%% -%% merlin.mbs (with options: `vonx,nm-rvvc,yr-par,jttl-rm,volp-com,jwdpg,jwdvol,numser,ser-vol,jnm-x,btit-rm,bt-rm,edparxc,bkedcap,au-col,in-col,fin-bare,pp,ed,abr,mth-bare,xedn,jabr,and-com,and-com-ed,xand,url,url-blk,em-x,nfss,') -%% ---------------------------------------- -%% *** Tentative .bst file for Springer LNCS *** -%% -%% Copyright 1994-2007 Patrick W Daly - % =============================================================== - % IMPORTANT NOTICE: - % This bibliographic style (bst) file has been generated from one or - % more master bibliographic style (mbs) files, listed above. - % - % This generated file can be redistributed and/or modified under the terms - % of the LaTeX Project Public License Distributed from CTAN - % archives in directory macros/latex/base/lppl.txt; either - % version 1 of the License, or any later version. - % =============================================================== - % Name and version information of the main mbs file: - % \ProvidesFile{merlin.mbs}[2007/04/24 4.20 (PWD, AO, DPC)] - % For use with BibTeX version 0.99a or later - %------------------------------------------------------------------- - % This bibliography style file is intended for texts in ENGLISH - % This is a numerical citation style, and as such is standard LaTeX. - % It requires no extra package to interface to the main text. - % The form of the \bibitem entries is - % \bibitem{key}... - % Usage of \cite is as follows: - % \cite{key} ==>> [#] - % \cite[chap. 2]{key} ==>> [#, chap. 2] - % where # is a number determined by the ordering in the reference list. - % The order in the reference list is alphabetical by authors. - %--------------------------------------------------------------------- - -ENTRY - { address - author - booktitle - chapter - edition - editor - eid - howpublished - institution - journal - key - month - note - number - organization - pages - publisher - school - series - title - type - url - volume - year - } - {} - { label } -INTEGERS { output.state before.all mid.sentence after.sentence after.block } -FUNCTION {init.state.consts} -{ #0 'before.all := - #1 'mid.sentence := - #2 'after.sentence := - #3 'after.block := -} -STRINGS { s t} -FUNCTION {output.nonnull} -{ 's := - output.state mid.sentence = - { ", " * write$ } - { output.state after.block = - { add.period$ write$ -% newline$ -% "\newblock " write$ % removed for titto-lncs-01 - " " write$ % to avoid long spaces between title and "In: ..." - } - { output.state before.all = - 'write$ - { add.period$ " " * write$ } - if$ - } - if$ - mid.sentence 'output.state := - } - if$ - s -} -FUNCTION {output} -{ duplicate$ empty$ - 'pop$ - 'output.nonnull - if$ -} -FUNCTION {output.check} -{ 't := - duplicate$ empty$ - { pop$ "empty " t * " in " * cite$ * warning$ } - 'output.nonnull - if$ -} -FUNCTION {fin.entry} -{ duplicate$ empty$ - 'pop$ - 'write$ - if$ - newline$ -} - -FUNCTION {new.block} -{ output.state before.all = - 'skip$ - { after.block 'output.state := } - if$ -} -FUNCTION {new.sentence} -{ output.state after.block = - 'skip$ - { output.state before.all = - 'skip$ - { after.sentence 'output.state := } - if$ - } - if$ -} -FUNCTION {add.blank} -{ " " * before.all 'output.state := -} - - -FUNCTION {add.colon} -{ duplicate$ empty$ - 'skip$ - { ":" * add.blank } - if$ -} - -FUNCTION {date.block} -{ - new.block -} - -FUNCTION {not} -{ { #0 } - { #1 } - if$ -} -FUNCTION {and} -{ 'skip$ - { pop$ #0 } - if$ -} -FUNCTION {or} -{ { pop$ #1 } - 'skip$ - if$ -} -STRINGS {z} -FUNCTION {remove.dots} -{ 'z := - "" - { z empty$ not } - { z #1 #1 substring$ - z #2 global.max$ substring$ 'z := - duplicate$ "." = 'pop$ - { * } - if$ - } - while$ -} -FUNCTION {new.block.checka} -{ empty$ - 'skip$ - 'new.block - if$ -} -FUNCTION {new.block.checkb} -{ empty$ - swap$ empty$ - and - 'skip$ - 'new.block - if$ -} -FUNCTION {new.sentence.checka} -{ empty$ - 'skip$ - 'new.sentence - if$ -} -FUNCTION {new.sentence.checkb} -{ empty$ - swap$ empty$ - and - 'skip$ - 'new.sentence - if$ -} -FUNCTION {field.or.null} -{ duplicate$ empty$ - { pop$ "" } - 'skip$ - if$ -} -FUNCTION {emphasize} -{ skip$ } -FUNCTION {tie.or.space.prefix} -{ duplicate$ text.length$ #3 < - { "~" } - { " " } - if$ - swap$ -} -FUNCTION {titto.space.prefix} % always introduce a space -{ duplicate$ text.length$ #3 < - { " " } - { " " } - if$ - swap$ -} - - -FUNCTION {capitalize} -{ "u" change.case$ "t" change.case$ } - -FUNCTION {space.word} -{ " " swap$ * " " * } - % Here are the language-specific definitions for explicit words. - % Each function has a name bbl.xxx where xxx is the English word. - % The language selected here is ENGLISH -FUNCTION {bbl.and} -{ "and"} - -FUNCTION {bbl.etal} -{ "et~al." } - -FUNCTION {bbl.editors} -{ "eds." } - -FUNCTION {bbl.editor} -{ "ed." } - -FUNCTION {bbl.edby} -{ "edited by" } - -FUNCTION {bbl.edition} -{ "edn." } - -FUNCTION {bbl.volume} -{ "vol." } - -FUNCTION {titto.bbl.volume} % for handling journals -{ "" } - -FUNCTION {bbl.of} -{ "of" } - -FUNCTION {bbl.number} -{ "no." } - -FUNCTION {bbl.nr} -{ "no." } - -FUNCTION {bbl.in} -{ "in" } - -FUNCTION {bbl.pages} -{ "pp." } - -FUNCTION {bbl.page} -{ "p." } - -FUNCTION {titto.bbl.pages} % for journals -{ "" } - -FUNCTION {titto.bbl.page} % for journals -{ "" } - -FUNCTION {bbl.chapter} -{ "chap." } - -FUNCTION {bbl.techrep} -{ "Tech. Rep." } - -FUNCTION {bbl.mthesis} -{ "Master's thesis" } - -FUNCTION {bbl.phdthesis} -{ "Ph.D. thesis" } - -MACRO {jan} {"Jan."} - -MACRO {feb} {"Feb."} - -MACRO {mar} {"Mar."} - -MACRO {apr} {"Apr."} - -MACRO {may} {"May"} - -MACRO {jun} {"Jun."} - -MACRO {jul} {"Jul."} - -MACRO {aug} {"Aug."} - -MACRO {sep} {"Sep."} - -MACRO {oct} {"Oct."} - -MACRO {nov} {"Nov."} - -MACRO {dec} {"Dec."} - -MACRO {acmcs} {"ACM Comput. Surv."} - -MACRO {acta} {"Acta Inf."} - -MACRO {cacm} {"Commun. ACM"} - -MACRO {ibmjrd} {"IBM J. Res. Dev."} - -MACRO {ibmsj} {"IBM Syst.~J."} - -MACRO {ieeese} {"IEEE Trans. Software Eng."} - -MACRO {ieeetc} {"IEEE Trans. Comput."} - -MACRO {ieeetcad} - {"IEEE Trans. Comput. Aid. Des."} - -MACRO {ipl} {"Inf. Process. Lett."} - -MACRO {jacm} {"J.~ACM"} - -MACRO {jcss} {"J.~Comput. Syst. Sci."} - -MACRO {scp} {"Sci. Comput. Program."} - -MACRO {sicomp} {"SIAM J. Comput."} - -MACRO {tocs} {"ACM Trans. Comput. Syst."} - -MACRO {tods} {"ACM Trans. Database Syst."} - -MACRO {tog} {"ACM Trans. Graphic."} - -MACRO {toms} {"ACM Trans. Math. Software"} - -MACRO {toois} {"ACM Trans. Office Inf. Syst."} - -MACRO {toplas} {"ACM Trans. Progr. Lang. Syst."} - -MACRO {tcs} {"Theor. Comput. Sci."} - -FUNCTION {bibinfo.check} -{ swap$ - duplicate$ missing$ - { - pop$ pop$ - "" - } - { duplicate$ empty$ - { - swap$ pop$ - } - { swap$ - pop$ - } - if$ - } - if$ -} -FUNCTION {bibinfo.warn} -{ swap$ - duplicate$ missing$ - { - swap$ "missing " swap$ * " in " * cite$ * warning$ pop$ - "" - } - { duplicate$ empty$ - { - swap$ "empty " swap$ * " in " * cite$ * warning$ - } - { swap$ - pop$ - } - if$ - } - if$ -} -FUNCTION {format.url} -{ url empty$ - { "" } -% { "\urlprefix\url{" url * "}" * } - { "\url{" url * "}" * } % changed in titto-lncs-02.bst - if$ -} - -INTEGERS { nameptr namesleft numnames } - - -STRINGS { bibinfo} - -FUNCTION {format.names} -{ 'bibinfo := - duplicate$ empty$ 'skip$ { - 's := - "" 't := - #1 'nameptr := - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { s nameptr - "{vv~}{ll}{, jj}{, f{.}.}" - format.name$ - bibinfo bibinfo.check - 't := - nameptr #1 > - { - namesleft #1 > - { ", " * t * } - { - s nameptr "{ll}" format.name$ duplicate$ "others" = - { 't := } - { pop$ } - if$ - "," * - t "others" = - { - " " * bbl.etal * - } - { " " * t * } - if$ - } - if$ - } - 't - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ - } if$ -} -FUNCTION {format.names.ed} -{ - 'bibinfo := - duplicate$ empty$ 'skip$ { - 's := - "" 't := - #1 'nameptr := - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { s nameptr - "{f{.}.~}{vv~}{ll}{ jj}" - format.name$ - bibinfo bibinfo.check - 't := - nameptr #1 > - { - namesleft #1 > - { ", " * t * } - { - s nameptr "{ll}" format.name$ duplicate$ "others" = - { 't := } - { pop$ } - if$ - "," * - t "others" = - { - - " " * bbl.etal * - } - { " " * t * } - if$ - } - if$ - } - 't - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ - } if$ -} -FUNCTION {format.authors} -{ author "author" format.names -} -FUNCTION {get.bbl.editor} -{ editor num.names$ #1 > 'bbl.editors 'bbl.editor if$ } - -FUNCTION {format.editors} -{ editor "editor" format.names duplicate$ empty$ 'skip$ - { - " " * - get.bbl.editor -% capitalize - "(" swap$ * ")" * - * - } - if$ -} -FUNCTION {format.note} -{ - note empty$ - { "" } - { note #1 #1 substring$ - duplicate$ "{" = - 'skip$ - { output.state mid.sentence = - { "l" } - { "u" } - if$ - change.case$ - } - if$ - note #2 global.max$ substring$ * "note" bibinfo.check - } - if$ -} - -FUNCTION {format.title} -{ title - duplicate$ empty$ 'skip$ - { "t" change.case$ } - if$ - "title" bibinfo.check -} -FUNCTION {output.bibitem} -{ newline$ - "\bibitem{" write$ - cite$ write$ - "}" write$ - newline$ - "" - before.all 'output.state := -} - -FUNCTION {n.dashify} -{ - 't := - "" - { t empty$ not } - { t #1 #1 substring$ "-" = - { t #1 #2 substring$ "--" = not - { "--" * - t #2 global.max$ substring$ 't := - } - { { t #1 #1 substring$ "-" = } - { "-" * - t #2 global.max$ substring$ 't := - } - while$ - } - if$ - } - { t #1 #1 substring$ * - t #2 global.max$ substring$ 't := - } - if$ - } - while$ -} - -FUNCTION {word.in} -{ bbl.in capitalize - ":" * - " " * } - -FUNCTION {format.date} -{ - month "month" bibinfo.check - duplicate$ empty$ - year "year" bibinfo.check duplicate$ empty$ - { swap$ 'skip$ - { "there's a month but no year in " cite$ * warning$ } - if$ - * - } - { swap$ 'skip$ - { - swap$ - " " * swap$ - } - if$ - * - remove.dots - } - if$ - duplicate$ empty$ - 'skip$ - { - before.all 'output.state := - " (" swap$ * ")" * - } - if$ -} -FUNCTION {format.btitle} -{ title "title" bibinfo.check - duplicate$ empty$ 'skip$ - { - } - if$ -} -FUNCTION {either.or.check} -{ empty$ - 'pop$ - { "can't use both " swap$ * " fields in " * cite$ * warning$ } - if$ -} -FUNCTION {format.bvolume} -{ volume empty$ - { "" } - { bbl.volume volume tie.or.space.prefix - "volume" bibinfo.check * * - series "series" bibinfo.check - duplicate$ empty$ 'pop$ - { emphasize ", " * swap$ * } - if$ - "volume and number" number either.or.check - } - if$ -} -FUNCTION {format.number.series} -{ volume empty$ - { number empty$ - { series field.or.null } - { output.state mid.sentence = - { bbl.number } - { bbl.number capitalize } - if$ - number tie.or.space.prefix "number" bibinfo.check * * - series empty$ - { "there's a number but no series in " cite$ * warning$ } - { bbl.in space.word * - series "series" bibinfo.check * - } - if$ - } - if$ - } - { "" } - if$ -} - -FUNCTION {format.edition} -{ edition duplicate$ empty$ 'skip$ - { - output.state mid.sentence = - { "l" } - { "t" } - if$ change.case$ - "edition" bibinfo.check - " " * bbl.edition * - } - if$ -} -INTEGERS { multiresult } -FUNCTION {multi.page.check} -{ 't := - #0 'multiresult := - { multiresult not - t empty$ not - and - } - { t #1 #1 substring$ - duplicate$ "-" = - swap$ duplicate$ "," = - swap$ "+" = - or or - { #1 'multiresult := } - { t #2 global.max$ substring$ 't := } - if$ - } - while$ - multiresult -} -FUNCTION {format.pages} -{ pages duplicate$ empty$ 'skip$ - { duplicate$ multi.page.check - { - bbl.pages swap$ - n.dashify - } - { - bbl.page swap$ - } - if$ - tie.or.space.prefix - "pages" bibinfo.check - * * - } - if$ -} -FUNCTION {format.journal.pages} -{ pages duplicate$ empty$ 'pop$ - { swap$ duplicate$ empty$ - { pop$ pop$ format.pages } - { - ", " * - swap$ - n.dashify - pages multi.page.check - 'titto.bbl.pages - 'titto.bbl.page - if$ - swap$ tie.or.space.prefix - "pages" bibinfo.check - * * - * - } - if$ - } - if$ -} -FUNCTION {format.journal.eid} -{ eid "eid" bibinfo.check - duplicate$ empty$ 'pop$ - { swap$ duplicate$ empty$ 'skip$ - { - ", " * - } - if$ - swap$ * - } - if$ -} -FUNCTION {format.vol.num.pages} % this function is used only for journal entries -{ volume field.or.null - duplicate$ empty$ 'skip$ - { -% bbl.volume swap$ tie.or.space.prefix - titto.bbl.volume swap$ titto.space.prefix -% rationale for the change above: for journals you don't want "vol." label -% hence it does not make sense to attach the journal number to the label when -% it is short - "volume" bibinfo.check - * * - } - if$ - number "number" bibinfo.check duplicate$ empty$ 'skip$ - { - swap$ duplicate$ empty$ - { "there's a number but no volume in " cite$ * warning$ } - 'skip$ - if$ - swap$ - "(" swap$ * ")" * - } - if$ * - eid empty$ - { format.journal.pages } - { format.journal.eid } - if$ -} - -FUNCTION {format.chapter.pages} -{ chapter empty$ - 'format.pages - { type empty$ - { bbl.chapter } - { type "l" change.case$ - "type" bibinfo.check - } - if$ - chapter tie.or.space.prefix - "chapter" bibinfo.check - * * - pages empty$ - 'skip$ - { ", " * format.pages * } - if$ - } - if$ -} - -FUNCTION {format.booktitle} -{ - booktitle "booktitle" bibinfo.check -} -FUNCTION {format.in.ed.booktitle} -{ format.booktitle duplicate$ empty$ 'skip$ - { -% editor "editor" format.names.ed duplicate$ empty$ 'pop$ % changed by titto - editor "editor" format.names duplicate$ empty$ 'pop$ - { - " " * - get.bbl.editor -% capitalize - "(" swap$ * ") " * - * swap$ - * } - if$ - word.in swap$ * - } - if$ -} -FUNCTION {empty.misc.check} -{ author empty$ title empty$ howpublished empty$ - month empty$ year empty$ note empty$ - and and and and and - key empty$ not and - { "all relevant fields are empty in " cite$ * warning$ } - 'skip$ - if$ -} -FUNCTION {format.thesis.type} -{ type duplicate$ empty$ - 'pop$ - { swap$ pop$ - "t" change.case$ "type" bibinfo.check - } - if$ -} -FUNCTION {format.tr.number} -{ number "number" bibinfo.check - type duplicate$ empty$ - { pop$ bbl.techrep } - 'skip$ - if$ - "type" bibinfo.check - swap$ duplicate$ empty$ - { pop$ "t" change.case$ } - { tie.or.space.prefix * * } - if$ -} -FUNCTION {format.article.crossref} -{ - key duplicate$ empty$ - { pop$ - journal duplicate$ empty$ - { "need key or journal for " cite$ * " to crossref " * crossref * warning$ } - { "journal" bibinfo.check emphasize word.in swap$ * } - if$ - } - { word.in swap$ * " " *} - if$ - " \cite{" * crossref * "}" * -} -FUNCTION {format.crossref.editor} -{ editor #1 "{vv~}{ll}" format.name$ - "editor" bibinfo.check - editor num.names$ duplicate$ - #2 > - { pop$ - "editor" bibinfo.check - " " * bbl.etal - * - } - { #2 < - 'skip$ - { editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" = - { - "editor" bibinfo.check - " " * bbl.etal - * - } - { - bbl.and space.word - * editor #2 "{vv~}{ll}" format.name$ - "editor" bibinfo.check - * - } - if$ - } - if$ - } - if$ -} -FUNCTION {format.book.crossref} -{ volume duplicate$ empty$ - { "empty volume in " cite$ * "'s crossref of " * crossref * warning$ - pop$ word.in - } - { bbl.volume - capitalize - swap$ tie.or.space.prefix "volume" bibinfo.check * * bbl.of space.word * - } - if$ - editor empty$ - editor field.or.null author field.or.null = - or - { key empty$ - { series empty$ - { "need editor, key, or series for " cite$ * " to crossref " * - crossref * warning$ - "" * - } - { series emphasize * } - if$ - } - { key * } - if$ - } - { format.crossref.editor * } - if$ - " \cite{" * crossref * "}" * -} -FUNCTION {format.incoll.inproc.crossref} -{ - editor empty$ - editor field.or.null author field.or.null = - or - { key empty$ - { format.booktitle duplicate$ empty$ - { "need editor, key, or booktitle for " cite$ * " to crossref " * - crossref * warning$ - } - { word.in swap$ * } - if$ - } - { word.in key * " " *} - if$ - } - { word.in format.crossref.editor * " " *} - if$ - " \cite{" * crossref * "}" * -} -FUNCTION {format.org.or.pub} -{ 't := - "" - address empty$ t empty$ and - 'skip$ - { - t empty$ - { address "address" bibinfo.check * - } - { t * - address empty$ - 'skip$ - { ", " * address "address" bibinfo.check * } - if$ - } - if$ - } - if$ -} -FUNCTION {format.publisher.address} -{ publisher "publisher" bibinfo.warn format.org.or.pub -} - -FUNCTION {format.organization.address} -{ organization "organization" bibinfo.check format.org.or.pub -} - -FUNCTION {article} -{ output.bibitem - format.authors "author" output.check - add.colon - new.block - format.title "title" output.check - new.block - crossref missing$ - { - journal - "journal" bibinfo.check - "journal" output.check - add.blank - format.vol.num.pages output - format.date "year" output.check - } - { format.article.crossref output.nonnull - format.pages output - } - if$ -% new.block - format.url output -% new.block - format.note output - fin.entry -} -FUNCTION {book} -{ output.bibitem - author empty$ - { format.editors "author and editor" output.check - add.colon - } - { format.authors output.nonnull - add.colon - crossref missing$ - { "author and editor" editor either.or.check } - 'skip$ - if$ - } - if$ - new.block - format.btitle "title" output.check - crossref missing$ - { format.bvolume output - new.block - new.sentence - format.number.series output - format.publisher.address output - } - { - new.block - format.book.crossref output.nonnull - } - if$ - format.edition output - format.date "year" output.check -% new.block - format.url output -% new.block - format.note output - fin.entry -} -FUNCTION {booklet} -{ output.bibitem - format.authors output - add.colon - new.block - format.title "title" output.check - new.block - howpublished "howpublished" bibinfo.check output - address "address" bibinfo.check output - format.date output -% new.block - format.url output -% new.block - format.note output - fin.entry -} - -FUNCTION {inbook} -{ output.bibitem - author empty$ - { format.editors "author and editor" output.check - add.colon - } - { format.authors output.nonnull - add.colon - crossref missing$ - { "author and editor" editor either.or.check } - 'skip$ - if$ - } - if$ - new.block - format.btitle "title" output.check - crossref missing$ - { - format.bvolume output - format.chapter.pages "chapter and pages" output.check - new.block - new.sentence - format.number.series output - format.publisher.address output - } - { - format.chapter.pages "chapter and pages" output.check - new.block - format.book.crossref output.nonnull - } - if$ - format.edition output - format.date "year" output.check -% new.block - format.url output -% new.block - format.note output - fin.entry -} - -FUNCTION {incollection} -{ output.bibitem - format.authors "author" output.check - add.colon - new.block - format.title "title" output.check - new.block - crossref missing$ - { format.in.ed.booktitle "booktitle" output.check - format.bvolume output - format.chapter.pages output - new.sentence - format.number.series output - format.publisher.address output - format.edition output - format.date "year" output.check - } - { format.incoll.inproc.crossref output.nonnull - format.chapter.pages output - } - if$ -% new.block - format.url output -% new.block - format.note output - fin.entry -} -FUNCTION {inproceedings} -{ output.bibitem - format.authors "author" output.check - add.colon - new.block - format.title "title" output.check - new.block - crossref missing$ - { format.in.ed.booktitle "booktitle" output.check - new.sentence % added by titto - format.bvolume output - format.pages output - new.sentence - format.number.series output - publisher empty$ - { format.organization.address output } - { organization "organization" bibinfo.check output - format.publisher.address output - } - if$ - format.date "year" output.check - } - { format.incoll.inproc.crossref output.nonnull - format.pages output - } - if$ -% new.block - format.url output -% new.block - format.note output - fin.entry -} -FUNCTION {conference} { inproceedings } -FUNCTION {manual} -{ output.bibitem - author empty$ - { organization "organization" bibinfo.check - duplicate$ empty$ 'pop$ - { output - address "address" bibinfo.check output - } - if$ - } - { format.authors output.nonnull } - if$ - add.colon - new.block - format.btitle "title" output.check - author empty$ - { organization empty$ - { - address new.block.checka - address "address" bibinfo.check output - } - 'skip$ - if$ - } - { - organization address new.block.checkb - organization "organization" bibinfo.check output - address "address" bibinfo.check output - } - if$ - format.edition output - format.date output -% new.block - format.url output -% new.block - format.note output - fin.entry -} - -FUNCTION {mastersthesis} -{ output.bibitem - format.authors "author" output.check - add.colon - new.block - format.btitle - "title" output.check - new.block - bbl.mthesis format.thesis.type output.nonnull - school "school" bibinfo.warn output - address "address" bibinfo.check output - format.date "year" output.check -% new.block - format.url output -% new.block - format.note output - fin.entry -} - -FUNCTION {misc} -{ output.bibitem - format.authors output - add.colon - title howpublished new.block.checkb - format.title output - howpublished new.block.checka - howpublished "howpublished" bibinfo.check output - format.date output -% new.block - format.url output -% new.block - format.note output - fin.entry - empty.misc.check -} -FUNCTION {phdthesis} -{ output.bibitem - format.authors "author" output.check - add.colon - new.block - format.btitle - "title" output.check - new.block - bbl.phdthesis format.thesis.type output.nonnull - school "school" bibinfo.warn output - address "address" bibinfo.check output - format.date "year" output.check -% new.block - format.url output -% new.block - format.note output - fin.entry -} - -FUNCTION {proceedings} -{ output.bibitem - editor empty$ - { organization "organization" bibinfo.check output - } - { format.editors output.nonnull } - if$ - add.colon - new.block - format.btitle "title" output.check - format.bvolume output - editor empty$ - { publisher empty$ - { format.number.series output } - { - new.sentence - format.number.series output - format.publisher.address output - } - if$ - } - { publisher empty$ - { - new.sentence - format.number.series output - format.organization.address output } - { - new.sentence - format.number.series output - organization "organization" bibinfo.check output - format.publisher.address output - } - if$ - } - if$ - format.date "year" output.check -% new.block - format.url output -% new.block - format.note output - fin.entry -} - -FUNCTION {techreport} -{ output.bibitem - format.authors "author" output.check - add.colon - new.block - format.title - "title" output.check - new.block - format.tr.number output.nonnull - institution "institution" bibinfo.warn output - address "address" bibinfo.check output - format.date "year" output.check -% new.block - format.url output -% new.block - format.note output - fin.entry -} - -FUNCTION {unpublished} -{ output.bibitem - format.authors "author" output.check - add.colon - new.block - format.title "title" output.check - format.date output -% new.block - format.url output -% new.block - format.note "note" output.check - fin.entry -} - -FUNCTION {default.type} { misc } -READ -FUNCTION {sortify} -{ purify$ - "l" change.case$ -} -INTEGERS { len } -FUNCTION {chop.word} -{ 's := - 'len := - s #1 len substring$ = - { s len #1 + global.max$ substring$ } - 's - if$ -} -FUNCTION {sort.format.names} -{ 's := - #1 'nameptr := - "" - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { s nameptr - "{ll{ }}{ ff{ }}{ jj{ }}" - format.name$ 't := - nameptr #1 > - { - " " * - namesleft #1 = t "others" = and - { "zzzzz" * } - { t sortify * } - if$ - } - { t sortify * } - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ -} - -FUNCTION {sort.format.title} -{ 't := - "A " #2 - "An " #3 - "The " #4 t chop.word - chop.word - chop.word - sortify - #1 global.max$ substring$ -} -FUNCTION {author.sort} -{ author empty$ - { key empty$ - { "to sort, need author or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { author sort.format.names } - if$ -} -FUNCTION {author.editor.sort} -{ author empty$ - { editor empty$ - { key empty$ - { "to sort, need author, editor, or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { editor sort.format.names } - if$ - } - { author sort.format.names } - if$ -} -FUNCTION {author.organization.sort} -{ author empty$ - { organization empty$ - { key empty$ - { "to sort, need author, organization, or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { "The " #4 organization chop.word sortify } - if$ - } - { author sort.format.names } - if$ -} -FUNCTION {editor.organization.sort} -{ editor empty$ - { organization empty$ - { key empty$ - { "to sort, need editor, organization, or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { "The " #4 organization chop.word sortify } - if$ - } - { editor sort.format.names } - if$ -} -FUNCTION {presort} -{ type$ "book" = - type$ "inbook" = - or - 'author.editor.sort - { type$ "proceedings" = - 'editor.organization.sort - { type$ "manual" = - 'author.organization.sort - 'author.sort - if$ - } - if$ - } - if$ - " " - * - year field.or.null sortify - * - " " - * - title field.or.null - sort.format.title - * - #1 entry.max$ substring$ - 'sort.key$ := -} -ITERATE {presort} -SORT -STRINGS { longest.label } -INTEGERS { number.label longest.label.width } -FUNCTION {initialize.longest.label} -{ "" 'longest.label := - #1 'number.label := - #0 'longest.label.width := -} -FUNCTION {longest.label.pass} -{ number.label int.to.str$ 'label := - number.label #1 + 'number.label := - label width$ longest.label.width > - { label 'longest.label := - label width$ 'longest.label.width := - } - 'skip$ - if$ -} -EXECUTE {initialize.longest.label} -ITERATE {longest.label.pass} -FUNCTION {begin.bib} -{ preamble$ empty$ - 'skip$ - { preamble$ write$ newline$ } - if$ - "\begin{thebibliography}{" longest.label * "}" * - write$ newline$ - "\providecommand{\url}[1]{\texttt{#1}}" - write$ newline$ - "\providecommand{\urlprefix}{URL }" - write$ newline$ -} -EXECUTE {begin.bib} -EXECUTE {init.state.consts} -ITERATE {call.type$} -FUNCTION {end.bib} -{ newline$ - "\end{thebibliography}" write$ newline$ -} -EXECUTE {end.bib} -%% End of customized bst file -%% -%% End of file `titto.bst'. - - diff --git a/splncs_srt.bst b/splncs_srt.bst deleted file mode 100644 index caacfc6..0000000 --- a/splncs_srt.bst +++ /dev/null @@ -1,1248 +0,0 @@ -% BibTeX bibliography style `splncs_srt' - -% An attempt to match the bibliography style required for use with -% numbered references in Springer Verlag's "Lecture Notes in Computer -% Science" series. (See Springer's documentation for llncs.sty for -% more details of the suggested reference format.) Note that this -% file will not work for author-year style citations. - -% Use \documentclass{llncs} and \bibliographystyle{splncs_srt}, and cite -% a reference with (e.g.) \cite{smith77} to get a "[1]" in the text. - -% Copyright (C) 1999 Jason Noble. -% Last updated: Friday 07 March 2006, 08:04:42 Frank Holzwarth, Springer -% Last modification: added sorting feature from plain.bst -% done by Tobias Heindel, FMI Uni-Stuttgart, June 13th, 2006 -% -% Originally based on the BibTeX standard bibliography style `unsrt' -% - -ENTRY - { address - author - booktitle - chapter - edition - editor - howpublished - institution - journal - key - month - note - number - organization - pages - publisher - school - series - title - type - volume - year - } - {} - { label } - -INTEGERS { output.state before.all mid.sentence after.sentence - after.block after.authors between.elements} - -FUNCTION {init.state.consts} -{ #0 'before.all := - #1 'mid.sentence := - #2 'after.sentence := - #3 'after.block := - #4 'after.authors := - #5 'between.elements := -} - -STRINGS { s t } - -FUNCTION {output.nonnull} -{ 's := - output.state mid.sentence = - { " " * write$ } - { output.state after.block = - { add.period$ write$ - newline$ - "\newblock " write$ - } - { - output.state after.authors = - { ": " * write$ - newline$ - "\newblock " write$ - } - { output.state between.elements = - { ", " * write$ } - { output.state before.all = - 'write$ - { add.period$ " " * write$ } - if$ - } - if$ - } - if$ - } - if$ - mid.sentence 'output.state := - } - if$ - s -} - -FUNCTION {output} -{ duplicate$ empty$ - 'pop$ - 'output.nonnull - if$ -} - -FUNCTION {output.check} -{ 't := - duplicate$ empty$ - { pop$ "empty " t * " in " * cite$ * warning$ } - 'output.nonnull - if$ -} - -FUNCTION {output.bibitem} -{ newline$ - "\bibitem{" write$ - cite$ write$ - "}" write$ - newline$ - "" - before.all 'output.state := -} - -FUNCTION {fin.entry} -{ write$ - newline$ -} - -FUNCTION {new.block} -{ output.state before.all = - 'skip$ - { after.block 'output.state := } - if$ -} - -FUNCTION {stupid.colon} -{ after.authors 'output.state := } - -FUNCTION {insert.comma} -{ output.state before.all = - 'skip$ - { between.elements 'output.state := } - if$ -} - -FUNCTION {new.sentence} -{ output.state after.block = - 'skip$ - { output.state before.all = - 'skip$ - { after.sentence 'output.state := } - if$ - } - if$ -} - -FUNCTION {not} -{ { #0 } - { #1 } - if$ -} - -FUNCTION {and} -{ 'skip$ - { pop$ #0 } - if$ -} - -FUNCTION {or} -{ { pop$ #1 } - 'skip$ - if$ -} - -FUNCTION {new.block.checka} -{ empty$ - 'skip$ - 'new.block - if$ -} - -FUNCTION {new.block.checkb} -{ empty$ - swap$ empty$ - and - 'skip$ - 'new.block - if$ -} - -FUNCTION {new.sentence.checka} -{ empty$ - 'skip$ - 'new.sentence - if$ -} - -FUNCTION {new.sentence.checkb} -{ empty$ - swap$ empty$ - and - 'skip$ - 'new.sentence - if$ -} - -FUNCTION {field.or.null} -{ duplicate$ empty$ - { pop$ "" } - 'skip$ - if$ -} - -FUNCTION {emphasize} -{ duplicate$ empty$ - { pop$ "" } - { "" swap$ * "" * } - if$ -} - -FUNCTION {bold} -{ duplicate$ empty$ - { pop$ "" } - { "\textbf{" swap$ * "}" * } - if$ -} - -FUNCTION {parens} -{ duplicate$ empty$ - { pop$ "" } - { "(" swap$ * ")" * } - if$ -} - -INTEGERS { nameptr namesleft numnames } - -FUNCTION {format.springer.names} -{ 's := - #1 'nameptr := - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { s nameptr "{vv~}{ll}{, jj}{, f{.}.}" format.name$ 't := - nameptr #1 > - { namesleft #1 > - { ", " * t * } - { numnames #1 > - { ", " * } - 'skip$ - if$ - t "others" = - { " et~al." * } - { "" * t * } - if$ - } - if$ - } - 't - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ -} - -FUNCTION {format.names} -{ 's := - #1 'nameptr := - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { s nameptr "{vv~}{ll}{, jj}{, f.}" format.name$ 't := - nameptr #1 > - { namesleft #1 > - { ", " * t * } - { numnames #2 > - { "," * } - 'skip$ - if$ - t "others" = - { " et~al." * } - { " \& " * t * } - if$ - } - if$ - } - 't - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ -} - -FUNCTION {format.authors} -{ author empty$ - { "" } - { author format.springer.names } - if$ -} - -FUNCTION {format.editors} -{ editor empty$ - { "" } - { editor format.springer.names - editor num.names$ #1 > - { ", eds." * } - { ", ed." * } - if$ - } - if$ -} - -FUNCTION {format.title} -{ title empty$ - { "" } - { title "t" change.case$ } - if$ -} - -FUNCTION {n.dashify} -{ 't := - "" - { t empty$ not } - { t #1 #1 substring$ "-" = - { t #1 #2 substring$ "--" = not - { "--" * - t #2 global.max$ substring$ 't := - } - { { t #1 #1 substring$ "-" = } - { "-" * - t #2 global.max$ substring$ 't := - } - while$ - } - if$ - } - { t #1 #1 substring$ * - t #2 global.max$ substring$ 't := - } - if$ - } - while$ -} - -FUNCTION {format.date} -{ year empty$ - { month empty$ - { "" } - { "there's a month but no year in " cite$ * warning$ - month - } - if$ - } - { month empty$ - 'year - { month " " * year * } - if$ - } - if$ -} - -FUNCTION {format.btitle} -{ title emphasize -} - -FUNCTION {tie.or.space.connect} -{ duplicate$ text.length$ #3 < - { "~" } - { " " } - if$ - swap$ * * -} - -FUNCTION {either.or.check} -{ empty$ - 'pop$ - { "can't use both " swap$ * " fields in " * cite$ * warning$ } - if$ -} - -FUNCTION {format.bvolume} -{ volume empty$ - { "" } - { "Volume" volume tie.or.space.connect - series empty$ - 'skip$ - { " of " * series emphasize * } - if$ - add.period$ - "volume and number" number either.or.check - } - if$ -} - -FUNCTION {format.number.series} -{ volume empty$ - { number empty$ - { series field.or.null } - { output.state mid.sentence = - { "number" } - { "Number" } - if$ - number tie.or.space.connect - series empty$ - { "there's a number but no series in " cite$ * warning$ } - { " in " * series * } - if$ - } - if$ - } - { "" } - if$ -} - -FUNCTION {format.edition} -{ edition empty$ - { "" } - { output.state mid.sentence = - { edition "l" change.case$ " edn." * } - { edition "t" change.case$ " edn." * } - if$ - } - if$ -} - -INTEGERS { multiresult } - -FUNCTION {multi.page.check} -{ 't := - #0 'multiresult := - { multiresult not - t empty$ not - and - } - { t #1 #1 substring$ - duplicate$ "-" = - swap$ duplicate$ "," = - swap$ "+" = - or or - { #1 'multiresult := } - { t #2 global.max$ substring$ 't := } - if$ - } - while$ - multiresult -} - -FUNCTION {format.pages} -{ pages empty$ - { "" } - { pages multi.page.check - { "" pages n.dashify tie.or.space.connect } - { "" pages tie.or.space.connect } - if$ - } - if$ -} - -FUNCTION {format.vol} -{ volume bold -} - -FUNCTION {format.vol.num} -{ volume bold -number empty$ -{ } -{ number "(" swap$ * * ")" * } -if$ -} - -FUNCTION {pre.format.pages} -{ pages empty$ - 'skip$ - { duplicate$ empty$ - { pop$ format.pages } - { " " * pages n.dashify * } - if$ - } - if$ -} - -FUNCTION {format.chapter.pages} -{ chapter empty$ - 'format.pages - { type empty$ - { "chapter" } - { type "l" change.case$ } - if$ - chapter tie.or.space.connect - pages empty$ - 'skip$ - { " " * format.pages * } - if$ - } - if$ -} - -FUNCTION {format.in.ed.booktitle} -{ booktitle empty$ - { "" } - { editor empty$ - { "In: " booktitle emphasize * } - { "In " format.editors * ": " * booktitle emphasize * } - if$ - } - if$ -} - -FUNCTION {empty.misc.check} -{ author empty$ title empty$ howpublished empty$ - month empty$ year empty$ note empty$ - and and and and and - { "all relevant fields are empty in " cite$ * warning$ } - 'skip$ - if$ -} - -FUNCTION {format.thesis.type} -{ type empty$ - 'skip$ - { pop$ - type "t" change.case$ - } - if$ -} - -FUNCTION {format.tr.number} -{ type empty$ - { "Technical Report" } - 'type - if$ - number empty$ - { "t" change.case$ } - { number tie.or.space.connect } - if$ -} - -FUNCTION {format.article.crossref} -{ key empty$ - { journal empty$ - { "need key or journal for " cite$ * " to crossref " * crossref * - warning$ - "" - } - { "In {\em " journal * "\/}" * } - if$ - } - { "In " key * } - if$ - " \cite{" * crossref * "}" * -} - -FUNCTION {format.crossref.editor} -{ editor #1 "{vv~}{ll}" format.name$ - editor num.names$ duplicate$ - #2 > - { pop$ " et~al." * } - { #2 < - 'skip$ - { editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" = - { " et~al." * } - { " and " * editor #2 "{vv~}{ll}" format.name$ * } - if$ - } - if$ - } - if$ -} - -FUNCTION {format.book.crossref} -{ volume empty$ - { "empty volume in " cite$ * "'s crossref of " * crossref * warning$ - "In " - } - { "Volume" volume tie.or.space.connect - " of " * - } - if$ - " \cite{" * crossref * "}" * -} - -FUNCTION {format.incoll.inproc.crossref} -{ editor empty$ - editor field.or.null author field.or.null = - or - { key empty$ - { booktitle empty$ - { "need editor, key, or booktitle for " cite$ * " to crossref " * - crossref * warning$ - "" - } - { "" } - if$ - } - { "" } - if$ - } - { "" } - if$ - " \cite{" * crossref * "}" * -} - -FUNCTION {and.the.note} -{ note output - note empty$ - 'skip$ - { add.period$ } - if$ -} - -FUNCTION {article} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - crossref missing$ - { journal emphasize "journal" output.check - format.vol.num output - format.date parens output - format.pages output - } - { format.article.crossref output.nonnull - format.pages output - } - if$ - and.the.note - fin.entry -} - -FUNCTION {book} -{ output.bibitem - author empty$ - { format.editors "author and editor" output.check } - { format.authors output.nonnull - crossref missing$ - { "author and editor" editor either.or.check } - 'skip$ - if$ - } - if$ - stupid.colon - format.btitle "title" output.check - new.sentence - crossref missing$ - { format.edition output - format.bvolume output - new.block - format.number.series output - new.sentence - publisher "publisher" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - } - { format.book.crossref output.nonnull - } - if$ - and.the.note - fin.entry -} - -FUNCTION {booklet} -{ output.bibitem - format.authors output - stupid.colon - format.title "title" output.check - howpublished address new.block.checkb - howpublished output - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - and.the.note - fin.entry -} - -FUNCTION {inbook} -{ output.bibitem - author empty$ - { format.editors "author and editor" output.check } - { format.authors output.nonnull - crossref missing$ - { "author and editor" editor either.or.check } - 'skip$ - if$ - } - if$ - stupid.colon - crossref missing$ - { chapter output - new.block - format.number.series output - new.sentence - "In:" output - format.btitle "title" output.check - new.sentence - format.edition output - format.bvolume output - publisher "publisher" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - } - { chapter output - new.block - format.incoll.inproc.crossref output.nonnull - } - if$ - format.pages output - and.the.note - fin.entry -} - -FUNCTION {incollection} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - crossref missing$ - { format.in.ed.booktitle "booktitle" output.check - new.sentence - format.bvolume output - format.number.series output - new.block - format.edition output - publisher "publisher" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - format.pages output - } - { format.incoll.inproc.crossref output.nonnull - format.chapter.pages output - } - if$ - and.the.note - fin.entry -} - -FUNCTION {inproceedings} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - crossref missing$ - { format.in.ed.booktitle "booktitle" output.check - new.sentence - format.bvolume output - format.number.series output - address empty$ - { organization publisher new.sentence.checkb - organization empty$ - 'skip$ - { insert.comma } - if$ - organization output - publisher empty$ - 'skip$ - { insert.comma } - if$ - publisher output - format.date parens output - } - { insert.comma - address output.nonnull - organization empty$ - 'skip$ - { insert.comma } - if$ - organization output - publisher empty$ - 'skip$ - { insert.comma } - if$ - publisher output - format.date parens output - } - if$ - } - { format.incoll.inproc.crossref output.nonnull - } - if$ - format.pages output - and.the.note - fin.entry -} - -FUNCTION {conference} { inproceedings } - -FUNCTION {manual} -{ output.bibitem - author empty$ - { organization empty$ - 'skip$ - { organization output.nonnull - address output - } - if$ - } - { format.authors output.nonnull } - if$ - stupid.colon - format.btitle "title" output.check - author empty$ - { organization empty$ - { address new.block.checka - address output - } - 'skip$ - if$ - } - { organization address new.block.checkb - organization output - address empty$ - 'skip$ - { insert.comma } - if$ - address output - } - if$ - new.sentence - format.edition output - format.date parens output - and.the.note - fin.entry -} - -FUNCTION {mastersthesis} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - "Master's thesis" format.thesis.type output.nonnull - school empty$ - 'skip$ - { insert.comma } - if$ - school "school" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - and.the.note - fin.entry -} - -FUNCTION {misc} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - howpublished new.block.checka - howpublished output - format.date parens output - and.the.note - fin.entry - empty.misc.check -} - -FUNCTION {phdthesis} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.btitle "title" output.check - new.block - "PhD thesis" format.thesis.type output.nonnull - school empty$ - 'skip$ - { insert.comma } - if$ - school "school" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - and.the.note - fin.entry -} - -FUNCTION {proceedings} -{ output.bibitem - editor empty$ - { organization empty$ - { "" } - { organization output - stupid.colon } - if$ - } - { format.editors output.nonnull - stupid.colon - } - if$ - format.btitle "title" output.check - new.block - crossref missing$ - { format.in.ed.booktitle "booktitle" output.check - new.sentence - format.bvolume output - format.number.series output - address empty$ - { organization publisher new.sentence.checkb - organization empty$ - 'skip$ - { insert.comma } - if$ - organization output - publisher empty$ - 'skip$ - { insert.comma } - if$ - publisher output - format.date parens output - } - { insert.comma - address output.nonnull - organization empty$ - 'skip$ - { insert.comma } - if$ - organization output - publisher empty$ - 'skip$ - { insert.comma } - if$ - publisher output - format.date parens output - } - if$ - } - { format.incoll.inproc.crossref output.nonnull - } - if$ - and.the.note - fin.entry -} - -FUNCTION {techreport} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - format.tr.number output.nonnull - institution empty$ - 'skip$ - { insert.comma } - if$ - institution "institution" output.check - address empty$ - 'skip$ - { insert.comma } - if$ - address output - format.date parens output - and.the.note - fin.entry -} - -FUNCTION {unpublished} -{ output.bibitem - format.authors "author" output.check - stupid.colon - format.title "title" output.check - new.block - note "note" output.check - format.date parens output - fin.entry -} - -FUNCTION {default.type} { misc } - -MACRO {jan} {"January"} - -MACRO {feb} {"February"} - -MACRO {mar} {"March"} - -MACRO {apr} {"April"} - -MACRO {may} {"May"} - -MACRO {jun} {"June"} - -MACRO {jul} {"July"} - -MACRO {aug} {"August"} - -MACRO {sep} {"September"} - -MACRO {oct} {"October"} - -MACRO {nov} {"November"} - -MACRO {dec} {"December"} - -MACRO {acmcs} {"ACM Computing Surveys"} - -MACRO {acta} {"Acta Informatica"} - -MACRO {cacm} {"Communications of the ACM"} - -MACRO {ibmjrd} {"IBM Journal of Research and Development"} - -MACRO {ibmsj} {"IBM Systems Journal"} - -MACRO {ieeese} {"IEEE Transactions on Software Engineering"} - -MACRO {ieeetc} {"IEEE Transactions on Computers"} - -MACRO {ieeetcad} - {"IEEE Transactions on Computer-Aided Design of Integrated Circuits"} - -MACRO {ipl} {"Information Processing Letters"} - -MACRO {jacm} {"Journal of the ACM"} - -MACRO {jcss} {"Journal of Computer and System Sciences"} - -MACRO {scp} {"Science of Computer Programming"} - -MACRO {sicomp} {"SIAM Journal on Computing"} - -MACRO {tocs} {"ACM Transactions on Computer Systems"} - -MACRO {tods} {"ACM Transactions on Database Systems"} - -MACRO {tog} {"ACM Transactions on Graphics"} - -MACRO {toms} {"ACM Transactions on Mathematical Software"} - -MACRO {toois} {"ACM Transactions on Office Information Systems"} - -MACRO {toplas} {"ACM Transactions on Programming Languages and Systems"} - -MACRO {tcs} {"Theoretical Computer Science"} - -READ - -%% Begin of addition of sorting (taken from CTAN plain.bst) -%% Tobias Heindel June 13th, 2006 - -FUNCTION {sortify} -{ purify$ - "l" change.case$ -} - -INTEGERS { len } - -FUNCTION {chop.word} -{ 's := - 'len := - s #1 len substring$ = - { s len #1 + global.max$ substring$ } - 's - if$ -} - -FUNCTION {sort.format.names} -{ 's := - #1 'nameptr := - "" - s num.names$ 'numnames := - numnames 'namesleft := - { namesleft #0 > } - { nameptr #1 > - { " " * } - 'skip$ - if$ - s nameptr "{vv{ } }{ll{ }}{ ff{ }}{ jj{ }}" format.name$ 't := - nameptr numnames = t "others" = and - { "et al" * } - { t sortify * } - if$ - nameptr #1 + 'nameptr := - namesleft #1 - 'namesleft := - } - while$ -} - -FUNCTION {sort.format.title} -{ 't := - "A " #2 - "An " #3 - "The " #4 t chop.word - chop.word - chop.word - sortify - #1 global.max$ substring$ -} - -FUNCTION {author.sort} -{ author empty$ - { key empty$ - { "to sort, need author or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { author sort.format.names } - if$ -} - -FUNCTION {author.editor.sort} -{ author empty$ - { editor empty$ - { key empty$ - { "to sort, need author, editor, or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { editor sort.format.names } - if$ - } - { author sort.format.names } - if$ -} - -FUNCTION {author.organization.sort} -{ author empty$ - { organization empty$ - { key empty$ - { "to sort, need author, organization, or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { "The " #4 organization chop.word sortify } - if$ - } - { author sort.format.names } - if$ -} - -FUNCTION {editor.organization.sort} -{ editor empty$ - { organization empty$ - { key empty$ - { "to sort, need editor, organization, or key in " cite$ * warning$ - "" - } - { key sortify } - if$ - } - { "The " #4 organization chop.word sortify } - if$ - } - { editor sort.format.names } - if$ -} - -FUNCTION {presort} -{ type$ "book" = - type$ "inbook" = - or - 'author.editor.sort - { type$ "proceedings" = - 'editor.organization.sort - { type$ "manual" = - 'author.organization.sort - 'author.sort - if$ - } - if$ - } - if$ - " " - * - year field.or.null sortify - * - " " - * - title field.or.null - sort.format.title - * - #1 entry.max$ substring$ - 'sort.key$ := -} - -ITERATE {presort} - -SORT - -%% End of addition for sorting - -STRINGS { longest.label } - -INTEGERS { number.label longest.label.width } - -FUNCTION {initialize.longest.label} -{ "" 'longest.label := - #1 'number.label := - #0 'longest.label.width := -} - -FUNCTION {longest.label.pass} -{ number.label int.to.str$ 'label := - number.label #1 + 'number.label := - label width$ longest.label.width > - { label 'longest.label := - label width$ 'longest.label.width := - } - 'skip$ - if$ -} - -EXECUTE {initialize.longest.label} - -ITERATE {longest.label.pass} - -FUNCTION {begin.bib} -{ preamble$ empty$ - 'skip$ - { preamble$ write$ newline$ } - if$ - "\begin{thebibliography}{" longest.label * "}" * write$ newline$ -} - -EXECUTE {begin.bib} - -EXECUTE {init.state.consts} - -ITERATE {call.type$} - -FUNCTION {end.bib} -{ newline$ - "\end{thebibliography}" write$ newline$ -} - -EXECUTE {end.bib} \ No newline at end of file diff --git a/sprmindx.sty b/sprmindx.sty deleted file mode 100644 index 06a7c9a..0000000 --- a/sprmindx.sty +++ /dev/null @@ -1,4 +0,0 @@ -delim_0 "\\idxquad " -delim_1 "\\idxquad " -delim_2 "\\idxquad " -delim_n ",\\,"