From 5104e38ee747fd1052ce21f3f9f2ecc778d590ba Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 2 Feb 2006 10:49:28 +0000 Subject: [PATCH] ported to the IEEE latex8 style --- helm/papers/system_T/Latex8.ps | 502 ++++++++++++++ helm/papers/system_T/Latex8.txt | 21 + helm/papers/system_T/latex8.bib | 29 + helm/papers/system_T/latex8.bst | 1124 +++++++++++++++++++++++++++++++ helm/papers/system_T/latex8.sty | 169 +++++ helm/papers/system_T/latex8.tex | 230 +++++++ helm/papers/system_T/t.tex | 176 ++--- 7 files changed, 2170 insertions(+), 81 deletions(-) create mode 100644 helm/papers/system_T/Latex8.ps create mode 100644 helm/papers/system_T/Latex8.txt create mode 100644 helm/papers/system_T/latex8.bib create mode 100644 helm/papers/system_T/latex8.bst create mode 100644 helm/papers/system_T/latex8.sty create mode 100644 helm/papers/system_T/latex8.tex diff --git a/helm/papers/system_T/Latex8.ps b/helm/papers/system_T/Latex8.ps new file mode 100644 index 000000000..391c3906a --- /dev/null +++ b/helm/papers/system_T/Latex8.ps @@ -0,0 +1,502 @@ +%!PS-Adobe-2.0 +%%Creator: dvips 5.47 Copyright 1986-91 Radical Eye Software +%%Title: latex8.dvi +%%Pages: 2 1 +%%BoundingBox: 0 0 612 792 +%%DocumentFonts: Times-Roman Times-Bold Times-Italic Helvetica-Bold +%%EndComments +%%BeginProcSet: /usr/local/lib/tex/ps/psfig.pro +/TeXscale { 65536 div } def + +/DocumentInitState [ matrix currentmatrix currentlinewidth currentlinecap +currentlinejoin currentdash currentgray currentmiterlimit ] cvx def + +/startTexFig { + /SavedState save def + userdict maxlength dict begin + currentpoint transform + + DocumentInitState setmiterlimit setgray setdash setlinejoin setlinecap + setlinewidth setmatrix + + itransform moveto + + /ury exch TeXscale def + /urx exch TeXscale def + /lly exch TeXscale def + /llx exch TeXscale def + /y exch TeXscale def + /x exch TeXscale def + + currentpoint /cy exch def /cx exch def + + /sx x urx llx sub div def % scaling for x + /sy y ury lly sub div def % scaling for y + + sx sy scale % scale by (sx,sy) + + cx sx div llx sub + cy sy div ury sub translate + + /DefFigCTM matrix currentmatrix def + + /initmatrix { + DefFigCTM setmatrix + } def + /defaultmatrix { + DefFigCTM exch copy + } def + + /initgraphics { + DocumentInitState setmiterlimit setgray setdash + setlinejoin setlinecap setlinewidth setmatrix + DefFigCTM setmatrix + } def + + /showpage { + initgraphics + } def + /erasepage { + initgraphics + } def + /copypage {} def + +} def +/clipFig { + currentpoint 6 2 roll + newpath 4 copy + + 4 2 roll moveto + 6 -1 roll exch lineto + exch lineto + exch lineto + closepath clip + newpath + moveto +} def +/doclip { llx lly urx ury clipFig } def +/endTexFig { + end SavedState restore +} def +%%EndProcSet +%%BeginProcSet: tex.pro +/TeXDict 200 dict def TeXDict begin /N /def load def /B{bind def}N /S /exch +load def /X{S N}B /TR /translate load N /isls false N /vsize 10 N /@rigin{ +isls{[0 1 -1 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale +Resolution VResolution vsize neg mul TR matrix currentmatrix dup dup 4 get +round 4 exch put dup dup 5 get round 5 exch put setmatrix}N /@letter{/vsize 10 +N}B /@landscape{/isls true N /vsize -1 N}B /@a4{/vsize 10.6929133858 N}B /@a3{ +/vsize 15.5531 N}B /@ledger{/vsize 16 N}B /@legal{/vsize 13 N}B /@manualfeed{ +statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0 0]N +/FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{/nn 8 dict N nn begin +/FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array +/BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2 +array copy cvx N load 0 nn put /ctr 0 N[}B /df{/sf 1 N /fntrx FMat N df-tail} +B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0]N df-tail}B /E{pop nn dup definefont +setfont}B /ch-width{ch-data dup length 5 sub get}B /ch-height{ch-data dup +length 4 sub get}B /ch-xoff{128 ch-data dup length 3 sub get sub}B /ch-yoff{ +ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B +/ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 +N /rw 0 N /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S +dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 +ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice +ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 add]{ch-image} +imagemask restore}B /D{/cc X dup type /stringtype ne{]}if nn /base get cc ctr +put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf +div put}if put /ctr ctr 1 add N}B /I{cc 1 add D}B /bop{userdict /bop-hook +known{bop-hook}if /SI save N @rigin 0 0 moveto}N /eop{clear SI restore +showpage userdict /eop-hook known{eop-hook}if}N /@start{userdict /start-hook +known{start-hook}if /VResolution X /Resolution X 1000 div /DVImag X /IE 256 +array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for}N /p /show load N +/RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X +/rulex X V}B /V statusdict begin /product where{pop product dup length 7 ge{0 +7 getinterval(Display)eq}{pop false}ifelse}{false}ifelse end{{gsave TR -.1 -.1 +TR 1 1 scale rulex ruley false RMat{BDot}imagemask grestore}}{{gsave TR -.1 +-.1 TR rulex ruley scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /a{ +moveto}B /delta 0 N /tail{dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{ +S p tail}B /c{-4 M}B /d{-3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B +/j{3 M}B /k{4 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p -1 w +}B /q{p 1 w}B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{3 2 roll p +a}B /bos{/SS save N}B /eos{clear SS restore}B end +%%EndProcSet +%%BeginProcSet: texps.pro +TeXDict begin /rf{655360 div mul Resolution mul 7227 div /PixPerEm X findfont +dup length 1 add dict /nn X{1 index /FID ne{nn 3 1 roll put}{pop pop}ifelse} +forall 256 dict begin nn /Encoding get 0 1 255{2 copy get 3 index 2 index get +1000 mul PixPerEm div def pop}for pop pop nn /Metrics currentdict put end +/fontname X /nn dup nn definefont[PixPerEm 0 0 PixPerEm neg 0 0]makefont N +fontname{/foo setfont}2 array copy cvx N fontname load 0 nn put}N +/ObliqueSlant{dup sin S cos div neg}B /SlantFont{/foo X[1 0 foo 1 0 0] +TransFont}N /ExtendFont{/foo X 3 2 roll[S{foo div}forall]3 1 roll[foo 0 0 1 0 + +0]TransFont}N /TransFont{S findfont S makefont dup length dict /nn X{1 index +/FID ne{nn 3 1 roll put}{pop pop}ifelse}forall dup nn definefont pop}N end +%%EndProcSet +TeXDict begin 1000 300 300 @start /Fa [ 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 9 12 16 19 19 31 +29 12 12 12 19 25 9 12 9 10 19 19 19 19 19 19 19 19 19 19 12 +12 25 25 25 19 34 23 23 25 27 23 23 27 27 12 17 25 21 31 25 +27 23 27 23 19 21 27 23 31 23 21 21 15 10 15 16 19 12 19 19 +17 19 17 10 19 19 10 10 17 10 27 19 19 19 19 15 15 10 19 17 +25 17 17 15 15 10 15 20 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 15 19 19 6 19 19 19 19 8 21 +19 12 12 19 19 0 19 19 19 9 0 20 13 12 21 21 19 33 37 0 19 +0 12 12 12 12 12 12 12 12 0 12 12 0 12 12 12 33 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 33 0 10 0 0 0 0 21 27 35 12 0 0 0 0 0 25 +0 0 0 10 0 0 10 19 25 19 0 0 0 0 ] /Times-Italic 1000 589824 +rf /Fb [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 9 12 15 19 19 31 29 12 12 12 19 21 9 12 9 10 +19 19 19 19 19 19 19 19 19 19 10 10 21 21 21 17 34 27 25 25 +27 23 21 27 27 12 15 27 23 33 27 27 21 27 25 21 23 27 27 35 +27 27 23 12 10 12 18 19 12 17 19 17 19 17 12 19 19 10 10 19 +10 29 19 19 19 19 12 15 10 19 19 27 19 19 17 18 7 18 20 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 12 19 19 6 19 19 19 19 7 17 19 12 12 21 21 0 19 19 19 9 +0 17 13 12 17 17 19 37 37 0 17 0 12 12 12 12 12 12 12 12 0 +12 12 0 12 12 12 37 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 33 0 10 +0 0 0 0 23 27 33 12 0 0 0 0 0 25 0 0 0 10 0 0 10 19 27 19 0 +0 0 0 ] /Times-Roman 1000 589824 rf /Fc [ 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 8 11 14 17 17 +28 26 11 11 11 17 19 8 11 8 9 17 17 17 17 17 17 17 17 17 17 +9 9 19 19 19 15 31 24 22 22 24 20 18 24 24 11 13 24 20 30 24 +24 18 24 22 18 20 24 24 31 24 24 20 11 9 11 16 17 11 15 17 +15 17 15 11 17 17 9 9 17 9 26 17 17 17 17 11 13 9 17 17 24 +17 17 15 16 7 16 18 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 11 17 17 6 17 17 17 17 6 15 17 +11 11 18 18 0 17 17 17 8 0 15 12 11 15 15 17 33 33 0 15 0 11 +11 11 11 11 11 11 11 0 11 11 0 11 11 11 33 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 30 0 9 0 0 0 0 20 24 30 10 0 0 0 0 0 22 0 0 +0 9 0 0 9 17 24 17 0 0 0 0 ] /Times-Roman 1000 524288 rf /Fd +[ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 6 8 10 12 12 21 19 8 8 8 12 14 6 8 6 7 12 12 12 12 12 +12 12 12 12 12 7 7 14 14 14 11 23 18 17 17 18 15 14 18 18 8 +10 18 15 22 18 18 14 18 17 14 15 18 18 24 18 18 15 8 7 8 12 +12 8 11 12 11 12 11 8 12 12 7 7 12 7 19 12 12 12 12 8 10 7 +12 12 18 12 12 11 12 5 12 13 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 8 12 12 4 12 12 12 12 +4 11 12 8 8 14 14 0 12 12 12 6 0 11 9 8 11 11 12 25 25 0 11 +0 8 8 8 8 8 8 8 8 0 8 8 0 8 8 8 25 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 22 0 7 0 0 0 0 15 18 22 8 0 0 0 0 0 17 0 0 0 7 0 0 +7 12 18 12 0 0 0 0 ] /Times-Roman 1000 393216 rf /Fe [ 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +7 10 12 15 15 24 23 10 10 10 15 16 7 10 7 8 15 15 15 15 15 +15 15 15 15 15 8 8 16 16 16 13 27 21 19 19 21 18 16 21 21 10 +11 21 18 26 21 21 16 21 19 16 18 21 21 27 21 21 18 10 8 10 +14 15 10 13 15 13 15 13 10 15 15 8 8 15 8 23 15 15 15 15 10 +11 8 15 15 21 15 15 13 14 6 14 16 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 10 15 15 5 15 15 +15 15 5 13 15 10 10 16 16 0 15 15 15 7 0 13 10 10 13 13 15 +29 29 0 13 0 10 10 10 10 10 10 10 10 0 10 10 0 10 10 10 29 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 26 0 8 0 0 0 0 18 21 26 9 0 +0 0 0 0 19 0 0 0 8 0 0 8 15 21 15 0 0 0 0 ] /Times-Roman 1000 +458752 rf /Ff [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 12 14 20 23 23 37 30 12 14 14 16 24 12 +14 12 12 23 23 23 23 23 23 23 23 23 23 14 14 24 24 24 25 40 + +30 30 30 30 28 25 32 30 12 23 30 25 35 30 32 28 32 30 28 25 +30 28 39 28 28 25 14 12 14 24 23 12 23 25 23 25 23 14 25 25 +12 12 23 12 37 25 25 25 25 16 23 14 25 23 32 23 23 21 16 12 +16 24 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 14 23 23 7 23 23 23 23 10 21 23 14 14 25 25 0 +23 23 23 12 0 23 15 12 21 21 23 42 42 0 25 0 14 14 14 14 14 +14 14 14 0 14 14 0 14 14 14 42 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 42 0 15 0 0 0 0 25 32 42 15 0 0 0 0 0 37 0 0 0 12 0 0 12 +25 39 25 0 0 0 0 ] /Helvetica-Bold 1000 655360 rf /Fg 1 3 df<400020C000606000 +C03001801803000C0600060C0003180001B00000E00000E00001B000031800060C000C06001803 +003001806000C0C0006040002013147A9320>2 D E /Fh 1 59 df<60F0F06004047C830C>58 +D E /Fi [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 11 15 25 23 23 46 38 15 15 15 23 26 11 15 11 +13 23 23 23 23 23 23 23 23 23 23 15 15 26 26 26 23 42 33 30 +33 33 30 28 36 36 18 23 36 30 43 33 36 28 36 33 25 30 33 33 +46 33 33 30 15 13 15 27 23 15 23 25 20 25 20 15 23 25 13 15 +25 13 38 25 23 25 25 20 18 15 25 23 33 23 23 20 18 10 18 24 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 15 23 23 8 23 23 23 23 13 23 23 15 15 25 25 0 23 23 +23 11 0 25 16 15 23 23 23 46 46 0 23 0 15 15 15 15 15 15 15 +15 0 15 15 0 15 15 15 46 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 46 +0 14 0 0 0 0 30 36 46 15 0 0 0 0 0 33 0 0 0 13 0 0 13 23 33 +25 0 0 0 0 ] /Times-Bold 1000 720896 rf /Fj [ 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 10 14 17 +21 21 35 32 14 14 14 21 23 10 14 10 12 21 21 21 21 21 21 21 +21 21 21 12 12 23 23 23 18 38 30 28 28 30 25 23 30 30 14 16 +30 25 37 30 30 23 30 28 23 25 30 30 39 30 30 25 14 12 14 19 +21 14 18 21 18 21 18 14 21 21 12 12 21 12 32 21 21 21 21 14 +16 12 21 21 30 21 21 18 20 8 20 22 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 14 21 21 7 21 21 +21 21 7 18 21 14 14 23 23 0 21 21 21 10 0 19 15 14 18 18 21 +42 42 0 18 0 14 14 14 14 14 14 14 14 0 14 14 0 14 14 14 42 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 37 0 11 0 0 0 0 25 30 37 13 +0 0 0 0 0 28 0 0 0 12 0 0 12 21 30 21 0 0 0 0 ] /Times-Roman +1000 655360 rf /Fk [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 10 14 17 21 21 35 32 14 14 14 21 +28 10 14 10 12 21 21 21 21 21 21 21 21 21 21 14 14 28 28 28 +21 38 25 25 28 30 25 25 30 30 14 18 28 23 35 28 30 25 30 25 +21 23 30 25 35 25 23 23 16 12 16 18 21 14 21 21 18 21 18 12 +21 21 12 12 18 12 30 21 21 21 21 16 16 12 21 18 28 18 18 16 +17 11 17 22 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 16 21 21 7 21 21 21 21 9 23 21 14 14 21 +21 0 21 21 21 10 0 22 15 14 23 23 21 37 42 0 21 0 14 14 14 +14 14 14 14 14 0 14 14 0 14 14 14 37 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 37 0 11 0 0 0 0 23 30 39 13 0 0 0 0 0 28 0 0 0 12 +0 0 12 21 28 21 0 0 0 0 ] /Times-Italic 1000 655360 rf /Fl +[ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 12 17 28 25 25 50 41 17 17 17 25 28 12 17 12 14 25 25 +25 25 25 25 25 25 25 25 17 17 28 28 28 25 46 36 33 36 36 33 +30 39 39 19 25 39 33 47 36 39 30 39 36 28 33 36 36 50 36 36 +33 17 14 17 29 25 17 25 28 22 28 22 17 25 28 14 17 28 14 41 +28 25 28 28 22 19 17 28 25 36 25 25 22 20 11 20 26 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +17 25 25 8 25 25 25 25 14 25 25 17 17 28 28 0 25 25 25 12 0 +27 17 17 25 25 25 50 50 0 25 0 17 17 17 17 17 17 17 17 0 17 +17 0 17 17 17 50 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 50 0 15 0 +0 0 0 33 39 50 16 0 0 0 0 0 36 0 0 0 14 0 0 14 25 36 28 0 0 +0 0 ] /Times-Bold 1000 786432 rf /Fm [ 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 12 17 20 25 25 +41 39 17 17 17 25 28 12 17 12 14 25 25 25 25 25 25 25 25 25 +25 14 14 28 28 28 22 46 36 33 33 36 30 28 36 36 17 19 36 30 +44 36 36 28 36 33 28 30 36 36 47 36 36 30 17 14 17 23 25 17 + +22 25 22 25 22 17 25 25 14 14 25 14 39 25 25 25 25 17 19 14 +25 25 36 25 25 22 24 10 24 27 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 17 25 25 8 25 25 25 25 +9 22 25 17 17 28 28 0 25 25 25 12 0 23 17 17 22 22 25 50 50 +0 22 0 17 17 17 17 17 17 17 17 0 17 17 0 17 17 17 50 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 44 0 14 0 0 0 0 30 36 44 15 0 0 0 +0 0 33 0 0 0 14 0 0 14 25 36 25 0 0 0 0 ] /Times-Roman 1000 +786432 rf /Fn 1 3 df<60000006F000000FF800001F7C00003E3E00007C1F0000F80F8001F0 +07C003E003E007C001E0078001F00F8000F81F00007C3E00003E7C00001FF800000FF0000007E0 +000007E000000FF000001FF800003E7C00007C3E0000F81F0001F00F8001E0078003E007C007C0 +03E00F8001F01F0000F83E00007C7C00003EF800001FF000000F600000062022769F35>2 +D E /Fo 4 59 df<000600001E0003FE00FFFE00FFFE007CFE0000FE0000FE0000FE0000FE0000 +FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000 +FE0000FE007FFFFE7FFFFE7FFFFE171C7B9B22>49 D<0C0003000F803F000FFFFE000FFFFC000F +FFF8000FFFF0000FFFE0000FFFC0000FFE00000E0000000E0000000E0000000E0000000E000000 +0E0000000E3FC0000EFFF0000FC0FC000F007E000C003F000C003F8000001F8000001FC000001F +C000001FE000001FE018001FE07C001FE0FE001FE0FE001FE0FE001FE0FE001FC0FC001FC07800 +1FC070003F8038003F001C007E000F81FC0007FFF80003FFE00000FF00001B297D9B22>53 +D<003FC00001FFF00003FFF80007C07C000F003E001F001F001E000F803E000F803E000F803E00 +0F803F000F803F000F803FC00F003FF01F001FFC1E001FFE3C000FFFF80007FFE00003FFF80001 +FFFC0001FFFE0007FFFF000F0FFF801E03FFC03E01FFC07C007FC07C001FE0F8000FE0F80007E0 +F80003E0F80003E0F80003E0F80003C07C0003C07C0007C03E0007803F000F001FC07E0007FFFC +0003FFF000007FC0001B297DA722>56 D<1C003E007F00FF80FF80FF807F003E001C0009097B88 +13>58 D E /Fp [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 15 19 32 29 29 58 48 19 19 19 29 33 15 +19 15 16 29 29 29 29 29 29 29 29 29 29 19 19 33 33 33 29 54 +42 39 42 42 39 36 45 45 23 29 45 39 55 42 45 36 45 42 32 39 +42 42 58 42 42 39 19 16 19 34 29 19 29 32 26 32 26 19 29 32 +16 19 32 16 48 32 29 32 32 26 23 19 32 29 42 29 29 26 23 13 +23 30 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 19 29 29 10 29 29 29 29 16 29 29 19 19 32 32 +0 29 29 29 15 0 31 20 19 29 29 29 58 58 0 29 0 19 19 19 19 +19 19 19 19 0 19 19 0 19 19 19 58 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 58 0 17 0 0 0 0 39 45 58 19 0 0 0 0 0 42 0 0 0 16 0 0 +16 29 42 32 0 0 0 0 ] /Times-Bold 1000 917504 rf /Fq [ 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +12 15 19 23 23 39 36 15 15 15 23 26 12 15 12 13 23 23 23 23 +23 23 23 23 23 23 13 13 26 26 26 21 43 34 31 31 34 28 26 34 +34 15 18 34 28 41 34 34 26 34 31 26 28 34 34 44 34 34 28 15 +13 15 22 23 15 21 23 21 23 21 15 23 23 13 13 23 13 36 23 23 +23 23 15 18 13 23 23 34 23 23 21 22 9 22 25 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 15 23 23 +8 23 23 23 23 8 21 23 15 15 26 26 0 23 23 23 12 0 21 16 15 +21 21 23 46 46 0 21 0 15 15 15 15 15 15 15 15 0 15 15 0 15 +15 15 46 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 41 0 13 0 0 0 0 28 +34 41 14 0 0 0 0 0 31 0 0 0 13 0 0 13 23 34 23 0 0 0 0 ] /Times-Roman +1000 734003 rf /Fr [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 0 0 0 15 19 24 29 29 48 45 19 19 19 29 +33 15 19 15 16 29 29 29 29 29 29 29 29 29 29 16 16 33 33 33 +26 54 42 39 39 42 36 32 42 42 19 23 42 36 52 42 42 32 42 39 +32 36 42 42 55 42 42 36 19 16 19 27 29 19 26 29 26 29 26 19 +29 29 16 16 29 16 45 29 29 29 29 19 23 16 29 29 42 29 29 26 +28 12 28 31 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 0 0 0 0 19 29 29 10 29 29 29 29 10 26 29 19 19 +32 32 0 29 29 29 15 0 26 20 19 26 26 29 58 58 0 26 0 19 19 +19 19 19 19 19 19 0 19 19 0 19 19 19 58 0 0 0 0 0 0 0 0 0 0 +0 0 0 0 0 0 52 0 16 0 0 0 0 36 42 52 18 0 0 0 0 0 39 0 0 0 + +16 0 0 16 29 42 29 0 0 0 0 ] /Times-Roman 1000 917504 rf end +%%EndProlog +%%BeginSetup +%%Feature: *Resolution 300 +TeXDict begin +%%EndSetup +%%Page: 1 1 +bop 69 187 a Fr(L)84 179 y Fq(A)109 187 y Fr(T)135 205 y(E)162 +187 y(X)15 b Fp(Author)g(Guidelines)h(for)29 b Fo(8:5)16 b +Fn(\002)g Fo(11)p Fp(-Inch)f(Pr)o(oceedings)f(Manuscripts)414 +371 y Fm(Paolo)e(Ienne)155 429 y(Swiss)h(Federal)f(Institute)f(of)h(T)m +(echnology)248 487 y(Microcomputing)f(Laboratory)91 545 y(IN-F)g(Ecublens,)j +(1015)e(Lausanne,)i(Switzerland)298 603 y(Paolo.Ienne@di.ep\257.ch)1294 +371 y(Second)f(Author)1330 429 y(Institution2)1128 487 y(First)e(line)i(of)f +(institution2)f(address)1100 545 y(Second)h(line)g(of)g(institution2)g +(address)1115 603 y(SecondAuthor@institution2.com)308 778 y +Fl(Abstract)-41 878 y Fk(The)h(ABSTRACT)h(is)e(to)g(be)i(in)e +(fully-justi\256ed)e(italicized)h(text,)-91 928 y(at)k(the)h(top)e(of)i(the)f +(left-hand)f(column,)j(below)e(the)g(author)g(and)-91 978 y(af\256liation)f +(information.)34 b(Use)18 b(the)g(wor)n(d)f(\252Abstract\272)h(as)f(the)-91 +1027 y(title,)c(in)f(12-point)f(T)n(imes,)j(boldface)e(type,)j(center)n(ed)f +(r)n(elative)g(to)-91 1077 y(the)g(column,)i(initially)c(capitalized.)28 +b(The)15 b(abstract)f(is)g(to)h(be)g(in)-91 1127 y(10-point,)g(single-spaced) +g(type.)33 b(The)16 b(abstract)f(may)h(be)g(up)g(to)-91 1177 +y(3)f(inches)g(\(7.62)g(cm\))g(long.)28 b(Leave)17 b(two)d(blank)g(lines)h +(after)f(the)-91 1227 y(Abstract,)c(then)g(begin)g(the)g(main)f(text.)-91 +1389 y Fl(1.)k(Intr)o(oduction)-41 1494 y Fj(Please)f(follow)e(the)i(steps)f +(outlined)f(below)h(when)h(submitting)-91 1544 y(your)c(manuscript)h(to)g +(the)h(IEEE)g(Computer)f(Society)g(Press.)15 b(Note)-91 1593 +y(there)g(have)h(been)f(some)h(changes)g(to)f(the)g(measurements)h(from)-91 +1643 y(previous)9 b(instructions.)-91 1756 y Fl(2.)k(Instructions)-41 +1861 y Fj(Please)e(read)g(the)f(following)e(carefully)m(.)-91 +1961 y Fi(2.1.)k(Language)-41 2062 y Fj(All)d(manuscripts)h(must)g(be)h(in)e +(English.)-91 2162 y Fi(2.2.)j(Printing)f(your)h(paper)-41 +2262 y Fj(Print)c(your)h(properly)f(formatted)h(text)g(on)h(high-quality)m(,) +d(8)p Fh(:)p Fj(5)g Fg(\002)-91 2312 y Fj(11-inch)g(white)g(printer)f(paper)n +(.)15 b(A4)8 b(paper)g(is)f(also)h(acceptable,)i(but)-91 2362 +y(please)k(leave)f(the)g(extra)g(0.5)g(inch)f(\(1.27)g(cm\))i(at)f(the)g +(BOTT)o(OM)-91 2412 y(of)d(the)g(page.)-91 2512 y Fi(2.3.)i(Margins)f(and)h +(page)g(numbering)-41 2613 y Fj(All)18 b(printed)g(material,)j(including)c +(text,)k(illustrations,)e(and)-91 2662 y(charts,)14 b(must)f(be)g(kept)g +(within)e(a)i(print)f(area)i(6-7/8)e(inches)h(\(17.5)987 778 +y(cm\))e(wide)g(by)f(8-7/8)g(inches)g(\(22.54)g(cm\))i(high.)j(Do)c(not)f +(write)g(or)987 828 y(print)j(anything)f(outside)h(the)h(print)f(area.)27 +b(Number)15 b(your)e(pages)987 878 y(lightly)m(,)k(in)f(pencil,)j(on)d(the)h +(upper)g(right-hand)e(corners)i(of)g(the)987 928 y(BACKS)9 +b(of)h(the)g(pages)h(\(for)e(example,)i(1/10,)f(2/10,)f(or)h(1)g(of)f(10,)i +(2)987 978 y(of)f(10,)g(and)g(so)g(forth\).)j(Please)f(do)d(not)g(write)h(on) +f(the)h(fronts)f(of)h(the)987 1027 y(pages,)h(nor)f(on)g(the)g(lower)g +(halves)g(of)g(the)g(backs)h(of)f(the)g(pages.)987 1136 y Fi(2.4.)i +(Formatting)f(your)h(paper)1037 1245 y Fj(All)17 b(text)h(must)h(be)f(in)g(a) +h(two-column)f(format.)39 b(The)19 b(total)987 1295 y(allowable)13 +b(width)g(of)g(the)h(text)f(area)i(is)f(6-7/8)e(inches)i(\(17.5)g(cm\))987 +1345 y(wide)9 b(by)f(8-7/8)g(inches)h(\(22.54)g(cm\))g(high.)14 +b(Columns)8 b(are)i(to)e(be)i(3-)987 1395 y(1/4)g(inches)h(\(8.25)g(cm\))h +(wide,)f(with)f(a)i(5/16)e(inch)g(\(0.8)h(cm\))h(space)987 +1445 y(between)17 b(them.)34 b(The)17 b(main)g(title)e(\(on)h(the)h(\256rst)f + +(page\))h(should)987 1494 y(begin)8 b(1.0)i(inch)e(\(2.54)h(cm\))h(from)f +(the)g(top)f(edge)i(of)e(the)h(page.)16 b(The)987 1544 y(second)9 +b(and)f(following)e(pages)j(should)e(begin)h(1.0)g(inch)g(\(2.54)g(cm\))987 +1594 y(from)j(the)g(top)f(edge.)18 b(On)11 b(all)g(pages,)h(the)f(bottom)f +(mar)o(gin)h(should)987 1644 y(be)f(1-1/8)f(inches)h(\(2.86)f(cm\))i(from)e +(the)h(bottom)e(edge)j(of)e(the)h(page)987 1694 y(for)g(8)p +Fh(:)p Fj(5)e Fg(\002)i Fj(11-inch)f(paper;)i(for)f(A4)g(paper)n(,)h +(approximately)f(1-5/8)987 1744 y(inches)g(\(4.13)g(cm\))h(from)f(the)g +(bottom)f(edge)i(of)f(the)g(page.)987 1853 y Fi(2.5.)i(T)m(ype-style)g(and)g +(fonts)1037 1962 y Fj(Wherever)f(T)o(imes)f(is)h(speci\256ed,)g(T)o(imes)g +(Roman)f(may)h(also)f(be)987 2011 y(used.)17 b(If)10 b(neither)g(is)h +(available)f(on)h(your)f(word)g(processor)n(,)i(please)987 +2061 y(use)i(the)g(font)f(closest)i(in)e(appearance)j(to)d(T)o(imes)i(that)e +(you)h(have)987 2111 y(access)e(to.)1037 2163 y(MAIN)j(TITLE.)j(Center)e(the) +f(title)g(1-3/8)f(inches)i(\(3.49)g(cm\))987 2212 y(from)d(the)g(top)g(edge)g +(of)g(the)h(\256rst)f(page.)24 b(The)14 b(title)e(should)g(be)i(in)987 +2262 y(T)o(imes)j(14-point,)g(boldface)f(type.)35 b(Capitalize)16 +b(the)h(\256rst)f(letter)987 2312 y(of)c(nouns,)h(pronouns,)f(verbs,)h +(adjectives,)g(and)g(adverbs;)g(do)f(not)987 2362 y(capitalize)g(articles,)g +(coordinate)f(conjunctions,)g(or)g(prepositions)987 2412 y(\(unless)f(the)g +(title)f(begins)h(with)f(such)i(a)g(word\).)j(Leave)e(two)e(blank)987 +2461 y(lines)g(after)g(the)g(title.)1037 2513 y(AUTHOR)c(NAME\(s\))g(and)g +(AFFILIA)-5 b(TION\(s\))6 b(are)g(to)g(be)g(ce)q(n-)987 2563 +y(tered)13 b(beneath)g(the)g(title)e(and)i(printed)f(in)g(T)o(imes)h +(12-point,)f(non-)987 2613 y(boldface)i(type.)26 b(This)14 +b(information)e(is)i(to)f(be)i(followed)d(by)i(two)987 2662 +y(blank)c(lines.)p eop +%%Page: 2 2 +bop -41 42 a Fj(The)13 b(ABSTRACT)f(and)h(MAIN)g(TEXT)g(are)h(to)e(be)h(in)f +(a)h(two-)-91 91 y(column)d(format.)-41 142 y(MAIN)g(TEXT)m(.)i(T)m(ype)f +(main)f(text)g(in)g(10-point)e(T)o(imes,)j(single-)-91 192 +y(spaced.)k(Do)6 b(NOT)g(use)g(double-spacing.)14 b(All)6 b(paragraphs)g +(should)-91 241 y(be)13 b(indented)f(1)h(pica)g(\(approx.)23 +b(1/6)12 b(inch)g(or)h(0.422)g(cm\).)24 b(Make)-91 291 y(sure)12 +b(your)f(text)g(is)g(fully)f(justi\256ed\320that)g(is,)i(\257ush)g(left)f +(and)g(\257ush)-91 341 y(right.)i(Please)8 b(do)f(not)f(place)i(any)f +(additional)f(blank)g(lines)h(between)-91 391 y(paragraphs.)27 +b(Figure)14 b(and)h(table)f(captions)g(should)f(be)h(10-point)-91 +441 y(Helvetica)c(boldface)h(type)e(as)i(in)113 572 y Ff(Figure)h(1.)f +(Example)g(of)h(caption.)-91 674 y Fj(Long)e(captions)g(should)f(be)h(set)h +(as)g(in)-41 805 y Ff(Figure)17 b(2.)f(Example)g(of)g(long)h(caption)g +(requiring)-41 855 y(more)e(than)h(one)f(line.)26 b(It)14 b(is)g(not)i(typed) +f(centered)-41 905 y(but)f(aligned)h(on)f(both)h(sides)f(and)h(indented)g +(with)-41 955 y(an)d(additional)f(margin)h(on)g(both)h(sides)f(of)f(1)h +(pica.)-91 1098 y Fj(Callouts)k(should)g(be)h(9-point)e(Helvetica,)20 +b(non-boldface)c(type.)-91 1148 y(Initially)11 b(capitalize)j(only)f(the)h +(\256rst)g(word)f(of)h(section)f(titles)g(and)-91 1198 y(\256rst-,)d +(second-,)h(and)f(third-order)e(headings.)-41 1248 y(FIRST)l(-ORDER)i +(HEADINGS.)h(\(For)f(example,)i Fl(1.)20 b(Intr)o(o-)-91 1298 +y(duction)p Fj(\))7 b(should)h(be)h(T)o(imes)g(12-point)e(boldface,)j +(initially)c(cap-)-91 1348 y(italized,)i(\257ush)h(left,)g(with)e(one)i +(blank)f(line)g(before,)i(and)e(one)h(blank)-91 1398 y(line)g(after)n(.)-41 +1448 y(SECOND-ORDER)23 b(HEADINGS.)i(\(For)f(example,)29 b +Fi(1.1.)-91 1498 y(Database)13 b(elements)p Fj(\))g(should)e(be)h(T)o(imes)h +(11-point)d(boldface,)-91 1548 y(initially)h(capitalized,)k(\257ush)f(left,)g + +(with)f(one)h(blank)g(line)f(before,)-91 1597 y(and)18 b(one)g(after)n(.)37 +b(If)18 b(you)f(require)h(a)g(third-order)e(heading)h(\(we)-91 +1647 y(discourage)11 b(it\),)h(use)g(10-point)d(T)o(imes,)k(boldface,)f +(initially)d(capi-)-91 1697 y(talized,)k(\257ush)f(left,)g(preceded)h(by)f +(one)g(blank)f(line,)i(followed)e(by)-91 1747 y(a)g(period)e(and)h(your)g +(text)f(on)h(the)g(same)i(line.)-91 1853 y Fi(2.6.)g(Footnotes)-41 +1958 y Fj(Please)c(use)g(footnotes)f(sparingly)454 1943 y Fe(1)476 +1958 y Fj(and)h(place)g(them)g(at)g(the)f(bot-)-91 2008 y(tom)g(of)h(the)g +(column)f(on)h(the)g(page)g(on)g(which)f(they)h(are)h(referenced.)-91 +2058 y(Use)i(T)o(imes)f(8-point)f(type,)h(single-spaced.)-91 +2163 y Fi(2.7.)i(Refer)o(ences)-41 2269 y Fj(List)d(and)g(number)h(all)f +(bibliographical)e(references)k(in)e(9-point)-91 2319 y(T)o(imes,)14 +b(single-spaced,)f(at)g(the)f(end)h(of)f(your)g(paper)n(.)22 +b(When)13 b(ref-)-91 2369 y(erenced)i(in)f(the)h(text,)g(enclose)g(the)f +(citation)g(number)g(in)g(square)-91 2419 y(brackets,)h(for)d(example)i([1].) +24 b(Where)14 b(appropriate,)f(include)f(the)-91 2468 y(name\(s\))f(of)f +(editors)f(of)h(referenced)i(books.)p -91 2505 394 2 v -46 +2532 a Fd(1)-31 2544 y Fc(Or)o(,)c(better)f(still,)j(try)e(to)f(avoid)g +(footnotes)g(altogether)n(.)k(T)n(o)d(help)f(your)g(readers,)-91 +2584 y(avoid)j(using)g(footnotes)g(altogether)g(and)g(include)h(necessary)e +(peripheral)h(obser)o(-)-91 2623 y(vations)f(in)h(the)f(text)h(\(within)g +(parentheses,)f(if)h(you)f(prefer)o(,)h(as)g(in)f(this)h(sentence\).)987 +42 y Fi(2.8.)i(Illustrations,)f(graphs,)h(and)g(photographs)1037 +145 y Fj(All)f(graphics)i(should)e(be)i(centered.)22 b(Y)l(our)12 +b(artwork)g(must)g(be)987 195 y(in)f(place)h(in)f(the)h(article)f +(\(preferably)g(printed)g(as)h(part)f(of)h(the)f(text)987 245 +y(rather)e(than)g(pasted)g(up\).)14 b(If)9 b(you)g(are)h(using)e(photographs) +f(and)j(are)987 295 y(able)k(to)e(have)i(halftones)f(made)h(at)g(a)g(print)d +(shop,)j(use)g(a)g(100-)f(or)987 345 y(110-line)c(screen.)16 +b(If)10 b(you)g(must)g(use)g(plain)g(photos,)f(they)h(must)g(be)987 +394 y(pasted)e(onto)g(your)f(manuscript.)15 b(Use)9 b(rubber)f(cement)h(to)f +(af)o(\256x)h(the)987 444 y(images)f(in)e(place.)15 b(Black)7 +b(and)g(white,)g(clear)n(,)i(glossy-\256nish)d(photos)987 494 +y(are)k(preferable)h(to)e(color)n(.)14 b(Supply)9 b(the)g(best)h(quality)e +(photographs)987 544 y(and)i(illustrations)d(possible.)15 b(Penciled)10 +b(lines)f(and)h(very)g(\256ne)h(lines)987 594 y(do)g(not)h(reproduce)g(well.) +19 b(Remember)n(,)c(the)d(quality)e(of)i(the)f(book)987 643 +y(cannot)h(be)h(better)f(than)g(the)h(originals)e(provided.)21 +b(Do)12 b(NOT)h(use)987 693 y(tape)d(on)g(your)g(pages!)987 +797 y Fi(2.9.)i(Color)1037 901 y Fj(The)i(use)h(of)f(color)f(on)h(interior)e +(pages)j(\(that)e(is,)i(pages)g(other)987 951 y(than)e(the)f(cover\))h(is)g +(prohibitively)d(expensive.)23 b(W)m(e)14 b(publish)d(in-)987 +1000 y(terior)h(pages)i(in)f(color)f(only)g(when)h(it)g(is)g(speci\256cally)g +(requested)987 1050 y(and)h(budgeted)f(for)g(by)g(the)h(conference)h(or)o +(ganizers.)25 b(DO)14 b(NOT)987 1100 y(SUBMIT)c(COLOR)g(IMAGES)g(IN)g(YOUR)g +(P)l(APERS)g(UNLESS)987 1150 y(SPECIFICALL)l(Y)g(INSTRUCTED)h(T)o(O)g(DO)f +(SO.)987 1254 y Fi(2.10.)i(Symbols)1037 1357 y Fj(If)19 b(your)g(word)f +(processor)i(or)f(typewriter)f(cannot)i(produce)987 1407 y(Greek)9 +b(letters,)g(mathematical)g(symbols,)g(or)g(other)f(graphical)g(ele-)987 +1457 y(ments,)13 b(please)g(use)f(pressure-sensitive)g(\(self-adhesive\))g +(rub-on)987 1507 y(symbols)i(or)g(letters)g(\(available)h(in)f(most)g +(stationery)g(stores,)i(art)987 1557 y(stores,)11 b(or)e(graphics)h(shops\).) +987 1660 y Fi(2.11.)i(Copyright)f(forms)1037 1764 y Fj(Y)l(ou)16 + +b(must)g(include)g(your)f(signed)h(IEEE)h(copyright)e(release)987 +1814 y(form)i(when)h(you)f(submit)g(your)g(\256nished)g(paper)n(.)37 +b(W)m(e)18 b(MUST)987 1864 y(have)d(this)f(form)h(before)g(your)f(paper)h +(can)h(be)f(published)e(in)i(the)987 1914 y(proceedings.)987 +2017 y Fi(2.12.)d(Conclusions)1037 2121 y Fj(Please)k(direct)g(any)f +(questions)g(to)g(the)g(production)f(editor)g(in)987 2171 y(char)o(ge)e(of)g +(these)g(proceedings)f(at)g(the)h(IEEE)g(Computer)f(Society)987 +2221 y(Press:)k(Phone)10 b(\(714\))g(821-8380,)e(or)i(Fax)h(\(714\))e +(761-1784.)987 2337 y Fl(Refer)o(ences)992 2441 y Fb([1])21 +b(I.)8 b(M.)g(Author)n(.)h(Some)d(related)h(article)h(I)f(wrote.)j +Fa(Some)c(Fine)h(Journal)p Fb(,)1056 2487 y(99\(7\):1\261100,)h(January)g +(1999.)992 2530 y([2])21 b(A.)8 b(N.)h(Expert.)i Fa(A)d(Book)e(He)i(W)n(r)o +(ote)p Fb(.)i(His)e(Publisher)o(,)g(Erewhon,)f(NC,)1056 2576 +y(1999.)930 2787 y Fj(2)p eop +%%Trailer +end +userdict /end-hook known{end-hook}if +%%EOF diff --git a/helm/papers/system_T/Latex8.txt b/helm/papers/system_T/Latex8.txt new file mode 100644 index 000000000..e68fe5010 --- /dev/null +++ b/helm/papers/system_T/Latex8.txt @@ -0,0 +1,21 @@ +========== file: LATEX.TXT ======================= + +The following files contain the LaTeX macros necessary for you to format +your paper based on the instructions/measurements in the INSTRUCT.TXT +attachment in our standard author kit for 8.5 x 11-inch proceedings. +The files appear in the following order: + +latex8.sty -- the style file +latex8.tex -- the main macro set +latex8.bib -- the sample bibliography macros +latex8.bst -- the bibliography main macro set +latex8ps.txt -- this file, when printed out, will give you a sample +of how your paper should look when it's finished. This file is in a +separate attachment from the first four LaTeX files. Remember to save +it as a .ps file and strip out any extraneous lines at the top of the +file to enable successful printing. + +Note that both current versions of LaTeX, 2e and 2.09, have the same +macros -- refer to the start of the latex8.sty file for the opening +statement for each. + diff --git a/helm/papers/system_T/latex8.bib b/helm/papers/system_T/latex8.bib new file mode 100644 index 000000000..4daa996ef --- /dev/null +++ b/helm/papers/system_T/latex8.bib @@ -0,0 +1,29 @@ + +% +% $Description: Sample bibliography$ +% +% $Author: ienne $ +% $Date: 1995/09/15 15:19:53 $ +% $Revision: 1.3 $ +% + +@Article{ex1, + author = "Author, Ivan Marc", + title = "Some Related Article {I} Wrote", + journal = "Some Fine Journal", + month = "January", + number = "7", + year = "1999", + volume = "99", + pages = "1-100", +} + + +@Book{ex2, + author = "Expert, Andreas Nikolaos", + title = "A Book He Wrote", + publisher = "His Publisher", + address = "Erewhon, NC", + year = "1999" +} + diff --git a/helm/papers/system_T/latex8.bst b/helm/papers/system_T/latex8.bst new file mode 100644 index 000000000..88e49bf41 --- /dev/null +++ b/helm/papers/system_T/latex8.bst @@ -0,0 +1,1124 @@ + +% --------------------------------------------------------------- +% +% $Id: latex8.bst,v 1.1 1995/09/15 15:13:49 ienne Exp $ +% +% by Paolo.Ienne@di.epfl.ch +% + +% --------------------------------------------------------------- +% +% no guarantee is given that the format corresponds perfectly to +% IEEE 8.5" x 11" Proceedings, but most features should be ok. +% +% --------------------------------------------------------------- +% +% `latex8' from BibTeX standard bibliography style `abbrv' +% version 0.99a for BibTeX versions 0.99a or later, LaTeX version 2.09. +% Copyright (C) 1985, all rights reserved. +% Copying of this file is authorized only if either +% (1) you make absolutely no changes to your copy, including name, or +% (2) if you do make changes, you name it something other than +% btxbst.doc, plain.bst, unsrt.bst, alpha.bst, and abbrv.bst. +% This restriction helps ensure that all standard styles are identical. +% The file btxbst.doc has the documentation for this style. + +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 } + +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$ + } + { 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 {output.bibitem} +{ newline$ + "\bibitem{" write$ + cite$ write$ + "}" write$ + newline$ + "" + before.all 'output.state := +} + +FUNCTION {fin.entry} +{ add.period$ + write$ + 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 {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$ "" } + { "{\em " swap$ * "}" * } + if$ +} + +INTEGERS { nameptr namesleft numnames } + +FUNCTION {format.names} +{ 's := + #1 'nameptr := + s num.names$ 'numnames := + numnames 'namesleft := + { namesleft #0 > } + { s nameptr "{f.~}{vv~}{ll}{, jj}" format.name$ 't := + nameptr #1 > + { namesleft #1 > + { ", " * t * } + { numnames #2 > + { "," * } + 'skip$ + if$ + t "others" = + { " et~al." * } + { " and " * t * } + if$ + } + if$ + } + 't + if$ + nameptr #1 + 'nameptr := + + namesleft #1 - 'namesleft := + } + while$ +} + +FUNCTION {format.authors} +{ author empty$ + { "" } + { author format.names } + if$ +} + +FUNCTION {format.editors} +{ editor empty$ + { "" } + { editor format.names + editor num.names$ #1 > + { ", editors" * } + { ", editor" * } + 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$ + "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$ " edition" * } + { edition "t" change.case$ " edition" * } + 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" pages n.dashify tie.or.space.connect } + { "page" pages tie.or.space.connect } + if$ + } + if$ +} + +FUNCTION {format.vol.num.pages} +{ volume field.or.null + number empty$ + 'skip$ + { "(" number * ")" * * + volume empty$ + { "there's a number but no volume in " cite$ * warning$ } + 'skip$ + if$ + } + if$ + 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 + key empty$ not 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$ + 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$ + "" * + } + { "{\em " * series * "\/}" * } + 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$ + { booktitle empty$ + { "need editor, key, or booktitle for " cite$ * " to crossref " * + crossref * warning$ + "" + } + { "In {\em " booktitle * "\/}" * } + if$ + } + { "In " key * } + if$ + } + { "In " format.crossref.editor * } + if$ + " \cite{" * crossref * "}" * +} + +FUNCTION {article} +{ output.bibitem + format.authors "author" output.check + new.block + format.title "title" output.check + new.block + crossref missing$ + { journal emphasize "journal" output.check + format.vol.num.pages output + format.date "year" output.check + } + { format.article.crossref output.nonnull + format.pages output + } + if$ + new.block + note output + 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$ + new.block + format.btitle "title" output.check + crossref missing$ + { format.bvolume output + new.block + format.number.series output + new.sentence + publisher "publisher" output.check + address output + } + { new.block + format.book.crossref output.nonnull + } + if$ + format.edition output + format.date "year" output.check + new.block + note output + fin.entry +} + +FUNCTION {booklet} +{ output.bibitem + format.authors output + new.block + format.title "title" output.check + howpublished address new.block.checkb + howpublished output + address output + format.date output + new.block + note output + 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$ + new.block + format.btitle "title" output.check + crossref missing$ + { format.bvolume output + format.chapter.pages "chapter and pages" output.check + new.block + format.number.series output + new.sentence + publisher "publisher" output.check + 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 + note output + fin.entry +} + +FUNCTION {incollection} +{ output.bibitem + format.authors "author" output.check + new.block + format.title "title" output.check + new.block + crossref missing$ + { format.in.ed.booktitle "booktitle" output.check + format.bvolume output + format.number.series output + format.chapter.pages output + new.sentence + publisher "publisher" output.check + address output + format.edition output + format.date "year" output.check + } + { format.incoll.inproc.crossref output.nonnull + format.chapter.pages output + } + if$ + new.block + note output + fin.entry +} + +FUNCTION {inproceedings} +{ output.bibitem + format.authors "author" output.check + new.block + format.title "title" output.check + new.block + crossref missing$ + { format.in.ed.booktitle "booktitle" output.check + format.bvolume output + format.number.series output + format.pages output + address empty$ + { organization publisher new.sentence.checkb + organization output + publisher output + format.date "year" output.check + } + { address output.nonnull + format.date "year" output.check + new.sentence + organization output + publisher output + } + if$ + } + { format.incoll.inproc.crossref output.nonnull + format.pages output + } + if$ + new.block + note output + 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$ + new.block + 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 output + } + if$ + format.edition output + format.date output + new.block + note output + fin.entry +} + +FUNCTION {mastersthesis} +{ output.bibitem + format.authors "author" output.check + new.block + format.title "title" output.check + new.block + "Master's thesis" format.thesis.type output.nonnull + school "school" output.check + address output + format.date "year" output.check + new.block + note output + fin.entry +} + +FUNCTION {misc} +{ output.bibitem + format.authors output + title howpublished new.block.checkb + format.title output + howpublished new.block.checka + howpublished output + format.date output + new.block + note output + fin.entry + empty.misc.check +} + +FUNCTION {phdthesis} +{ output.bibitem + format.authors "author" output.check + new.block + format.btitle "title" output.check + new.block + "PhD thesis" format.thesis.type output.nonnull + school "school" output.check + address output + format.date "year" output.check + new.block + note output + fin.entry +} + +FUNCTION {proceedings} +{ output.bibitem + editor empty$ + { organization output } + { format.editors output.nonnull } + + if$ + new.block + format.btitle "title" output.check + format.bvolume output + format.number.series output + address empty$ + { editor empty$ + { publisher new.sentence.checka } + { organization publisher new.sentence.checkb + organization output + } + if$ + publisher output + format.date "year" output.check + } + { address output.nonnull + format.date "year" output.check + new.sentence + editor empty$ + 'skip$ + { organization output } + if$ + publisher output + } + if$ + new.block + note output + fin.entry +} + +FUNCTION {techreport} +{ output.bibitem + format.authors "author" output.check + new.block + format.title "title" output.check + new.block + format.tr.number output.nonnull + institution "institution" output.check + address output + format.date "year" output.check + new.block + note output + fin.entry +} + +FUNCTION {unpublished} +{ output.bibitem + format.authors "author" output.check + new.block + format.title "title" output.check + new.block + note "note" output.check + format.date output + fin.entry +} + +FUNCTION {default.type} { misc } + +MACRO {jan} {"Jan."} + +MACRO {feb} {"Feb."} + +MACRO {mar} {"Mar."} + +MACRO {apr} {"Apr."} + +MACRO {may} {"May"} + +MACRO {jun} {"June"} + +MACRO {jul} {"July"} + +MACRO {aug} {"Aug."} + +MACRO {sep} {"Sept."} + +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. Softw. Eng."} + +MACRO {ieeetc} {"IEEE Trans. Comput."} + +MACRO {ieeetcad} + {"IEEE Trans. Comput.-Aided Design Integrated Circuits"} + +MACRO {ipl} {"Inf. Process. Lett."} + +MACRO {jacm} {"J.~ACM"} + +MACRO {jcss} {"J.~Comput. Syst. Sci."} + +MACRO {scp} {"Sci. Comput. Programming"} + +MACRO {sicomp} {"SIAM J. Comput."} + +MACRO {tocs} {"ACM Trans. Comput. Syst."} + +MACRO {tods} {"ACM Trans. Database Syst."} + +MACRO {tog} {"ACM Trans. Gr."} + +MACRO {toms} {"ACM Trans. Math. Softw."} + +MACRO {toois} {"ACM Trans. Office Inf. Syst."} + +MACRO {toplas} {"ACM Trans. Prog. Lang. Syst."} + +MACRO {tcs} {"Theoretical Comput. Sci."} + +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 > } + { nameptr #1 > + { " " * } + 'skip$ + if$ + s nameptr "{vv{ } }{ll{ }}{ f{ }}{ 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 + +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 * + "}\setlength{\itemsep}{-1ex}\small" * 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 file latex8.bst +% --------------------------------------------------------------- + + + diff --git a/helm/papers/system_T/latex8.sty b/helm/papers/system_T/latex8.sty new file mode 100644 index 000000000..531053a4a --- /dev/null +++ b/helm/papers/system_T/latex8.sty @@ -0,0 +1,169 @@ + +% --------------------------------------------------------------- +% +% $Id: latex8.sty,v 1.2 1995/09/15 15:31:13 ienne Exp $ +% +% by Paolo.Ienne@di.epfl.ch +% +% --------------------------------------------------------------- +% +% no guarantee is given that the format corresponds perfectly to +% IEEE 8.5" x 11" Proceedings, but most features should be ok. +% +% --------------------------------------------------------------- +% with LaTeX2e: +% ============= +% +% use as +% \documentclass[times,10pt,twocolumn]{article} +% \usepackage{latex8} +% \usepackage{times} +% +% --------------------------------------------------------------- + +% with LaTeX 2.09: +% ================ +% +% use as +% \documentstyle[times,art10,twocolumn,latex8]{article} +% +% --------------------------------------------------------------- +% with both versions: +% =================== +% +% specify \pagestyle{empty} to omit page numbers in the final +% version +% +% specify references as +% \bibliographystyle{latex8} +% \bibliography{...your files...} +% +% use Section{} and SubSection{} instead of standard section{} +% and subsection{} to obtain headings in the form +% "1.3. My heading" +% +% --------------------------------------------------------------- + +\typeout{IEEE 8.5 x 11-Inch Proceedings Style `latex8.sty'.} + +% ten point helvetica bold required for captions +% in some sites the name of the helvetica bold font may differ, +% change the name here: +\font\tenhv = phvb at 10pt +%\font\tenhv = phvb7t at 10pt + +% eleven point times bold required for second-order headings +% \font\elvbf = cmbx10 scaled 1100 +\font\elvbf = ptmb scaled 1100 + +% set dimensions of columns, gap between columns, and paragraph indent +\setlength{\textheight}{8.875in} +\setlength{\textwidth}{6.875in} +\setlength{\columnsep}{0.3125in} +\setlength{\topmargin}{0in} +\setlength{\headheight}{0in} +\setlength{\headsep}{0in} +\setlength{\parindent}{1pc} +\setlength{\oddsidemargin}{-.304in} +\setlength{\evensidemargin}{-.304in} + +% memento from size10.clo +% \normalsize{\@setfontsize\normalsize\@xpt\@xiipt} +% \small{\@setfontsize\small\@ixpt{11}} +% \footnotesize{\@setfontsize\footnotesize\@viiipt{9.5}} +% \scriptsize{\@setfontsize\scriptsize\@viipt\@viiipt} +% \tiny{\@setfontsize\tiny\@vpt\@vipt} +% \large{\@setfontsize\large\@xiipt{14}} +% \Large{\@setfontsize\Large\@xivpt{18}} +% \LARGE{\@setfontsize\LARGE\@xviipt{22}} +% \huge{\@setfontsize\huge\@xxpt{25}} +% \Huge{\@setfontsize\Huge\@xxvpt{30}} + +\def\@maketitle + { + \newpage + \null + \vskip .375in + \begin{center} + {\Large \bf \@title \par} + % additional two empty lines at the end of the title + \vspace*{24pt} + { + \large + \lineskip .5em + \begin{tabular}[t]{c} + \@author + \end{tabular} + \par + } + % additional small space at the end of the author name + \vskip .5em + { + \large + \begin{tabular}[t]{c} + \@affiliation + \end{tabular} + \par + \ifx \@empty \@email + \else + \begin{tabular}{r@{~}l} + E-mail: & {\tt \@email} + \end{tabular} + \par + \fi + } + % additional empty line at the end of the title block + \vspace*{12pt} + \end{center} + } + +\def\abstract + {% + \centerline{\large\bf Abstract}% + \vspace*{12pt}% + \it% + } + +\def\endabstract + { + % additional empty line at the end of the abstract + \vspace*{12pt} + } + +\def\affiliation#1{\gdef\@affiliation{#1}} \gdef\@affiliation{} + +\def\email#1{\gdef\@email{#1}} +\gdef\@email{} + +\newlength{\@ctmp} +\newlength{\@figindent} +\setlength{\@figindent}{1pc} + +\long\def\@makecaption#1#2{ + \vskip 10pt + \setbox\@tempboxa\hbox{\tenhv\noindent #1.~#2} + \setlength{\@ctmp}{\hsize} + \addtolength{\@ctmp}{-\@figindent}\addtolength{\@ctmp}{-\@figindent} + % IF longer than one indented paragraph line + \ifdim \wd\@tempboxa >\@ctmp + % THEN set as an indented paragraph + \begin{list}{}{\leftmargin\@figindent \rightmargin\leftmargin} + \item[]\tenhv #1.~#2\par + \end{list} + \else + % ELSE center + \hbox to\hsize{\hfil\box\@tempboxa\hfil} + \fi} + +% correct heading spacing and type +\def\section{\@startsection {section}{1}{\z@} + {14pt plus 2pt minus 2pt}{14pt plus 2pt minus 2pt} {\large\bf}} +\def\subsection{\@startsection {subsection}{2}{\z@} + {13pt plus 2pt minus 2pt}{13pt plus 2pt minus 2pt} {\elvbf}} + +% add the period after section numbers +\newcommand{\Section}[1]{\section{\hskip -1em.~#1}} +\newcommand{\SubSection}[1]{\subsection{\hskip -1em.~#1}} + +% end of file latex8.sty +% --------------------------------------------------------------- diff --git a/helm/papers/system_T/latex8.tex b/helm/papers/system_T/latex8.tex new file mode 100644 index 000000000..fc401d6f3 --- /dev/null +++ b/helm/papers/system_T/latex8.tex @@ -0,0 +1,230 @@ + +% +% $Description: Author guidelines and sample document in LaTeX 2.09$ +% +% $Author: ienne $ +% $Date: 1995/09/15 15:20:59 $ +% $Revision: 1.4 $ +% + +\documentclass[times, 10pt,twocolumn]{article} +\usepackage{latex8} +\usepackage{times} + +%\documentstyle[times,art10,twocolumn,latex8]{article} + +%------------------------------------------------------------------------- +% take the % away on next line to produce the final camera-ready version +\pagestyle{empty} + +%------------------------------------------------------------------------- +\begin{document} + +\title{\LaTeX\ Author Guidelines + for {\boldmath $8.5 \times 11$-Inch} Proceedings Manuscripts} + +\author{Paolo Ienne\\ +Swiss Federal Institute of Technology\\ Microcomputing Laboratory \\ IN-F +Ecublens, 1015 Lausanne, Switzerland\\ Paolo.Ienne@di.epfl.ch\\ +% For a paper whose authors are all at the same institution, +% omit the following lines up until the closing ``}''. +% Additional authors and addresses can be added with ``\and'', +% just like the second author. +\and +Second Author\\ +Institution2\\ +First line of institution2 address\\ Second line of institution2 address\\ +SecondAuthor@institution2.com\\ +} + +\maketitle +\thispagestyle{empty} + +\begin{abstract} + The ABSTRACT is to be in fully-justified italicized text, at the top + of the left-hand column, below the author and affiliation + information. Use the word ``Abstract'' as the title, in 12-point + Times, boldface type, centered relative to the column, initially + capitalized. The abstract is to be in 10-point, single-spaced type. + The abstract may be up to 3 inches (7.62 cm) long. Leave two blank + lines after the Abstract, then begin the main text. +\end{abstract} + + + +%------------------------------------------------------------------------- +\Section{Introduction} + +Please follow the steps outlined below when submitting your +manuscript to the IEEE Computer Society Press. Note there have +been some changes to the measurements from previous instructions. + +%------------------------------------------------------------------------- +\Section{Instructions} + +Please read the following carefully. + +%------------------------------------------------------------------------- +\SubSection{Language} + +All manuscripts must be in English. + +%------------------------------------------------------------------------- +\SubSection{Printing your paper} + +Print your properly formatted text on high-quality, $8.5 \times 11$-inch +white printer paper. A4 paper is also acceptable, but please leave the +extra 0.5 inch (1.27 cm) at the BOTTOM of the page. + +%------------------------------------------------------------------------- +\SubSection{Margins and page numbering} + +All printed material, including text, illustrations, and charts, must be +kept within a print area 6-7/8 inches (17.5 cm) wide by 8-7/8 inches +(22.54 cm) high. Do not write or print anything outside the print area. +Number your pages lightly, in pencil, on the upper right-hand corners of +the BACKS of the pages (for example, 1/10, 2/10, or 1 of 10, 2 of 10, and +so forth). Please do not write on the fronts of the pages, nor on the +lower halves of the backs of the pages. + + +%------------------------------------------------------------------------ +\SubSection{Formatting your paper} + +All text must be in a two-column format. The total allowable width of +the text area is 6-7/8 inches (17.5 cm) wide by 8-7/8 inches (22.54 cm) +high. Columns are to be 3-1/4 inches (8.25 cm) wide, with a 5/16 inch +(0.8 cm) space between them. The main title (on the first page) should +begin 1.0 inch (2.54 cm) from the top edge of the page. The second and +following pages should begin 1.0 inch (2.54 cm) from the top edge. On +all pages, the bottom margin should be 1-1/8 inches (2.86 cm) from the +bottom edge of the page for $8.5 \times 11$-inch paper; for A4 paper, +approximately 1-5/8 inches (4.13 cm) from the bottom edge of the page. + +%------------------------------------------------------------------------- +\SubSection{Type-style and fonts} + +Wherever Times is specified, Times Roman may also be used. If neither is +available on your word processor, please use the font closest in +appearance to Times that you have access to. + +MAIN TITLE. Center the title 1-3/8 inches (3.49 cm) from the top edge of +the first page. The title should be in Times 14-point, boldface type. +Capitalize the first letter of nouns, pronouns, verbs, adjectives, and +adverbs; do not capitalize articles, coordinate conjunctions, or +prepositions (unless the title begins with such a word). Leave two blank +lines after the title. + +AUTHOR NAME(s) and AFFILIATION(s) are to be centered beneath the title +and printed in Times 12-point, non-boldface type. This information is to +be followed by two blank lines. + +The ABSTRACT and MAIN TEXT are to be in a two-column format. + +MAIN TEXT. Type main text in 10-point Times, single-spaced. Do NOT use +double-spacing. All paragraphs should be indented 1 pica (approx. 1/6 +inch or 0.422 cm). Make sure your text is fully justified---that is, +flush left and flush right. Please do not place any additional blank +lines between paragraphs. Figure and table captions should be 10-point +Helvetica boldface type as in +\begin{figure}[h] + \caption{Example of caption.} +\end{figure} + +\noindent Long captions should be set as in +\begin{figure}[h] + \caption{Example of long caption requiring more than one line. It is + not typed centered but aligned on both sides and indented with an + additional margin on both sides of 1~pica.} +\end{figure} + +\noindent Callouts should be 9-point Helvetica, non-boldface type. +Initially capitalize only the first word of section titles and first-, +second-, and third-order headings. + +FIRST-ORDER HEADINGS. (For example, {\large \bf 1. Introduction}) +should be Times 12-point boldface, initially capitalized, flush left, +with one blank line before, and one blank line after. + +SECOND-ORDER HEADINGS. (For example, {\elvbf 1.1. Database elements}) +should be Times 11-point boldface, initially capitalized, flush left, +with one blank line before, and one after. If you require a third-order +heading (we discourage it), use 10-point Times, boldface, initially +capitalized, flush left, preceded by one blank line, followed by a period +and your text on the same line. + +%------------------------------------------------------------------------- +\SubSection{Footnotes} + +Please use footnotes sparingly% +\footnote + {% + Or, better still, try to avoid footnotes altogether. To help your + readers, avoid using footnotes altogether and include necessary + peripheral observations in the text (within parentheses, if you + prefer, as in this sentence). + } +and place them at the bottom of the column on the page on which they are +referenced. Use Times 8-point type, single-spaced. + + +%------------------------------------------------------------------------- +\SubSection{References} + +List and number all bibliographical references in 9-point Times, +single-spaced, at the end of your paper. When referenced in the text, +enclose the citation number in square brackets, for example~\cite{ex1}. +Where appropriate, include the name(s) of editors of referenced books. + +%------------------------------------------------------------------------- +\SubSection{Illustrations, graphs, and photographs} + +All graphics should be centered. Your artwork must be in place in the +article (preferably printed as part of the text rather than pasted up). +If you are using photographs and are able to have halftones made at a +print shop, use a 100- or 110-line screen. If you must use plain photos, +they must be pasted onto your manuscript. Use rubber cement to affix the +images in place. Black and white, clear, glossy-finish photos are +preferable to color. Supply the best quality photographs and +illustrations possible. Penciled lines and very fine lines do not +reproduce well. Remember, the quality of the book cannot be better than +the originals provided. Do NOT use tape on your pages! + +%------------------------------------------------------------------------- +\SubSection{Color} + +The use of color on interior pages (that is, pages other +than the cover) is prohibitively expensive. We publish interior pages in +color only when it is specifically requested and budgeted for by the +conference organizers. DO NOT SUBMIT COLOR IMAGES IN YOUR +PAPERS UNLESS SPECIFICALLY INSTRUCTED TO DO SO. + +%------------------------------------------------------------------------- +\SubSection{Symbols} + +If your word processor or typewriter cannot produce Greek letters, +mathematical symbols, or other graphical elements, please use +pressure-sensitive (self-adhesive) rub-on symbols or letters (available +in most stationery stores, art stores, or graphics shops). + +%------------------------------------------------------------------------ +\SubSection{Copyright forms} + +You must include your signed IEEE copyright release form when you submit +your finished paper. We MUST have this form before your paper can be +published in the proceedings. + +%------------------------------------------------------------------------- +\SubSection{Conclusions} + +Please direct any questions to the production editor in charge of these +proceedings at the IEEE Computer Society Press: Phone (714) 821-8380, or +Fax (714) 761-1784. + +%------------------------------------------------------------------------- +\nocite{ex1,ex2} +\bibliographystyle{latex8} +\bibliography{latex8} + +\end{document} + diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index 9d5622d2b..42b937bf2 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -1,9 +1,14 @@ -\documentclass[a4paper]{article} +\documentclass[times, 10pt,twocolumn, draft]{article} \pagestyle{headings} %\usepackage{graphicx} \usepackage{amssymb,amsmath,mathrsfs,stmaryrd,amsthm} %\usepackage{hyperref} %\usepackage{picins} +\usepackage{latex8} +\usepackage{times} + +\pagestyle{empty} + \newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}} \newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket} @@ -35,13 +40,14 @@ \begin{document} \maketitle +\thispagestyle{empty} \begin{abstract} ... \end{abstract} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Introduction} +\Section{Introduction} The characterization of the provable recursive functions of Peano Arithmetic as the terms of system T is a well known result of G\"odel \cite{Godel58,Godel90}. Although several authors acknowledge @@ -108,7 +114,7 @@ logic and adding little by little small bits of logical power. This paper is the first step in this direction. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{G\"odel system T} +\Section{G\"odel system T} We shall use a variant of system T with three atomic types $\N$ (natural numbers), $\B$ (booleans) and $\one$ (a terminal object), and two binary type constructors $\times$ (product) and $\to$ (arrow type). @@ -120,19 +126,24 @@ with explicit pairs, plus the following additional constants: \item $true: \B$, $false:\B$, $D:A\to A \to \B \to A$ \item $O:\N$, $S:\N \to \N$, $R:A \to (A \to \N \to A) \to \N \to A$, \end{itemize} -Redexes comprise $\beta$-reduction -\[(\beta)~~ \lambda x:U.M ~ N \leadsto M[N/x]\] -projections - -\[(\pi_1)~~fst \pair{M}{N} \leadsto M\\ \hspace{.6cm} (\pi_2)~~ snd \pair{M}{N} -\leadsto N \] -and the following type specific reductions: -\[(D_{true})~~\\D~M~N~ true \leadsto M \hspace{.6cm} - (D_{false})~~ D~M~N~false \leadsto N \] -\[(R_0)~~\\R~M~F~ 0 \leadsto M \hspace{.6cm} - (R_S)~~ R~M~F~(S~n) \leadsto F~n~(R~M~F~n) \] -\[(*)~~ M \leadsto * \] -where (*) holds for any $M$ of type $\one$. +Redexes comprise $\beta$-reduction, projections, +and type specific reductions as reported in table \ref{tab:tredex} + +\begin{table}[!h] +\hrule\vspace{0.1cm} +\begin{tabular}{p{0.34\textwidth}r} + $\lambda x:U.M ~ N \leadsto M[N/x]$ & $(\beta)$ \\ + $fst \pair{M}{N} \leadsto M$ & $(\pi_1)$ \\ + $snd \pair{M}{N} \leadsto N$ & $(\pi_2)$ \\ + $D~M~N~ true \leadsto M$ & $(D_{true})$ \\ + $D~M~N~false \leadsto N$ & $(D_{false})$ \\ + $R~M~F~ 0 \leadsto M$ & $(R_0)$ \\ + $R~M~F~(S~n) \leadsto F~n~(R~M~F~n)$ & $(R_S)$ \\ + $M \leadsto * ~~~~ $ for any M of type $\one$ & $(*)$ +\end{tabular}\vspace{0.1cm} +\hrule +\caption{\label{tab:tredex}Reduction rules for System T} +\end{table} Note that using the well known isomorpshims $\one \to A \cong A$, $A \to \one \cong \one$ @@ -144,9 +155,7 @@ to realize atomic proposition, and stripping out the terminal object using the above isomorphisms gives a simple way of just keeping the truly informative part of the algorithms. - - -\section{Heyting's arithmetics} +\Section{Heyting's arithmetics} {\bf Axioms} @@ -170,18 +179,23 @@ informative part of the algorithms. {\bf Inference Rules} say that ax:AX refers to the previous Axioms list... - -\[ - (Proj)\hspace{0.1cm} \Gamma, x:A, \Delta \vdash x:A - \hspace{2cm} - (Const)\hspace{0.1cm} \Gamma \vdash ax : AX -\] - -\[ - (\to_i)\hspace{0.1cm}\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm} - (\to_e)\hspace{0.1cm}\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A} - {\Gamma \vdash M N: Q} -\] +\begin{table}[!h] +\hrule\vspace{0.1cm} +\begin{tabular}{p{0.34\textwidth}r} + $\Gamma, x:A, \Delta \vdash x:A$ & $(Proj)$\\ + $\Gamma \vdash ax : AX$ & $(Const)$\\ + $\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q}$ & + $(\to_i)$\\ + $\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A} + {\Gamma \vdash M N: Q}$ & $(\to_e)$\\ + $\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*)$ & + $(\forall_i)$\\ + $\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}$ & + $(\forall_e)$ +\end{tabular}\vspace{0.1cm} +\hrule +\caption{\label{tab:HArules}Inference rules} +\end{table}{lr} %\[ % (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B} @@ -192,12 +206,6 @@ say that ax:AX refers to the previous Axioms list... % (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B} %\] -\[ - (\forall_i)\hspace{0.1cm}\frac{\Gamma \vdash M:P}{\Gamma \vdash - \lambda x:\N.M: \forall x.P}(*) \hspace{2cm} - (\forall_e)\hspace{0.1cm}\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]} -\] - %\[ % (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm} @@ -205,7 +213,7 @@ say that ax:AX refers to the previous Axioms list... %{\Gamma \vdash Q} %\] -\section{Extraction} +\Section{Extraction} The formulae to types translation function $\sem{\cdot}$, see table \ref{tab:formulae2types}, takes in input formulae in HA and returns @@ -216,7 +224,7 @@ canoniac element is formed. \begin{table}[!h] \hrule\vspace{0.1cm} -\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}} +\begin{tabular}{p{0.21\textwidth}p{0.21\textwidth}} $\sem{A} = \one$ if A is atomic & $\sem{A \land B} = \sem{A}\times \sem{B}$ \\ $\sem{A \to B} = \sem{A}\to \sem{B}$ & @@ -229,11 +237,11 @@ canoniac element is formed. \begin{table}[!h] \hrule\vspace{0.1cm} -\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}} +\begin{tabular}{p{0.20\textwidth}p{0.20\textwidth}} $\semT{M N} = \semT{M} \semT{N}$ & - $\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$ \\ - $\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$ & - $\semT{M t} = \semT{M} \semT{t}$ + $\semT{M t} = \semT{M} \semT{t}$ \\ + \multicolumn{2}{l}{$\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$} \\ + \multicolumn{2}{l}{$\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$} \end{tabular}\vspace{0.1cm} \hrule \caption{\label{tab:structproof}Structured proofs} @@ -241,26 +249,19 @@ canoniac element is formed. \begin{table}[!h] \hrule\vspace{0.1cm} -\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}} - $\sem{fst} = \pi_1$& +\begin{tabular}{l}%{0.47\textwidth}p{0.47\textwidth}} + $\sem{fst} = \pi_1$\\ $\sem{snd} = \pi_2$\\ - $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$& + $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$\\ $\sem{false\_ind} = \canonical_{\sem{Q}}$\\ - $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$& + $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$\\ $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$\\ - $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$& + $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$\\ $\sem{nat\_ind} = R$ \\ - \multicolumn{2}{l}{ - $\sem{plus\_S} = \sem{times\_S} = \lambda \_:\N. \lambda \_:\N.\star$ - }\\ - \multicolumn{2}{l}{ - $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$ - }\\ - \multicolumn{2}{l}{ - $\sem{ex\_ind} = - \lambda f:(\N \to \sem{P} \to \sem{Q}). - \lambda p:\N\times \sem{P}.f~(fst~p)~(snd~p)$. - } + $\sem{plus\_S} = \sem{times\_S} = \lambda \_:\N. \lambda \_:\N.\star$ \\ + $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$ \\ + $\sem{ex\_ind} = \lambda f:(\N \to \sem{P} \to \sem{Q}).$\\ + $\qquad\lambda p:\N\times \sem{P}.f~(fst~p)~(snd~p)$ \end{tabular}\vspace{0.1cm} \hrule \caption{\label{tab:axioms}Axioms translation} @@ -268,11 +269,11 @@ canoniac element is formed. \begin{table}[!h] \hrule\vspace{0.1cm} -\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}} - $\canonical_\one = \lambda x:\one.x$ & +\begin{tabular}{l}%p{0.23\textwidth}p{0.23\textwidth}} + $\canonical_\one = \lambda x:\one.x$ \\ $\canonical_N = \lambda x:\one.0$ \\ $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U} - x}{\canonical_{V} x}$ & + x}{\canonical_{V} x}$ \\ $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$ \end{tabular}\vspace{0.1cm} \hrule @@ -280,7 +281,7 @@ canoniac element is formed. \end{table} -\section{Realizability} +\Section{Realizability} The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and $P$ is a closed formula. In particular: @@ -429,8 +430,10 @@ realizers):\\ Let us assume $h : \forall m.(\forall p. p < m \to P~p) \to P~m$. We prove by induction on $n$ that $\forall q. q \le n \to P~q$. For $n=0$, we get a proof of $P ~q$ by -\[ B \equiv \lambda q.\lambda h_0:q \le 0. h ~q~ -(\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \] +\begin{eqnarray} +B & \equiv & \lambda q.\lambda h_0:q \le 0. h ~q~ \nonumber\\ +& & \quad (\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \nonumber +\end{eqnarray} In the inductive case, we must prove that, for any $n$, \[(\forall q. q \le n \to P~q) \to (\forall q. q \le S n \to P~q)\] Assume $h_1: \forall q. q \le n \to P q$ and @@ -439,12 +442,18 @@ If $h_3: p < q$ then $(M~ p~ q~ n~ h_3~ h_2): p \le n$, hence $h_1 ~p ~ (M~ p~ q~ n~ h_3~ h_2): P~p$.\\ In conclusion, the proof of the inductive case is -\[I \equiv \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n. -h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2)) \] +\begin{eqnarray} +I & \equiv & \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n. \nonumber\\ + & & \quad h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2)) + \nonumber +\end{eqnarray} (where $h$ is free in I). The full proof is -\[ \lambda h: \forall m.(\forall p. p < m \to P~p) \to P~m.\lambda m. -nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) \] +\begin{eqnarray} +& \lambda h:\forall m.(\forall p. p < m\to P~p)\to P~m.\lambda m. &\nonumber\\ +& \quad nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) & \nonumber +\end{eqnarray} + where $le\_n$ is a proof that $\forall n. n \le n$, and the free $P$ in the definition of $nat_{ind}$ is instantiated with $\forall m.m \le m \to P~m$.\\ Form the previous proof,after stripping terminal objects, and a bit of eta-contraction to make @@ -460,8 +469,10 @@ $F[h]: A$. This defines a functional $f: \lambda q.\lambda g.F[g]: N\to(N\to A) \to A$, such that (morally) $h$ is the fixpoint of $f$. For instance, in the case of the fibonacci function, $f$ is -\[fibo \equiv \lambda q. \lambda g. -if~ q = 0~then~ 1~ else~ if~ q = 1~ then~ 1~ else~ g (q-1)+g (q-2)\] +\begin{eqnarray} +fibo & \equiv & \lambda q. \lambda g. if~ q = 0~then~ 1~ else \nonumber\\ +& & \quad if~ q = 1~ then~ 1~ else ~ g (q-1)+g (q-2) \nonumber +\end{eqnarray} So $f$ build a new approximation of $h$ from the previous approximation $h$ taken @@ -529,7 +540,7 @@ il $\lambda h2$ essendo $[[q <= Sn]]$ = 1 viene scartata. se si spiega come array viene decente... forse. lunedi' provo a scrivere meglio. -\section{Inductive types} +\Section{Inductive types} The notation we will use is similar to the one used in \cite{Werner} and \cite{Paulin89} but we prefer giving a label to each constructor and use that label instead of the @@ -543,7 +554,7 @@ $A \to \vec{B} \to C$ is a shortcut for $A \to B_1 \to \ldots \to B_n \to C$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Extensions to the logic framework} +\SubSection{Extensions to the logic framework} To talk about arbitrary inductive types (and not hard coded natural numbers) we have to extend a bit our framework. @@ -562,13 +573,13 @@ The definition of $\R$ is modified substituting each occurrence of $\N$ with a generic inductive type $T$. %%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Type definition} +\SubSection{Type definition} $$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$ $$C(X) ::= X \| T \to C(X) \| X \to C(X)$$ In the second case we mean $T \neq X$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Induction principle} +\SubSection{Induction principle} The induction principle for an inductive type $X$ and a predicate $Q$ is a constant with the following type $$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(t)$$ @@ -583,8 +594,8 @@ constructor of X, and $c:C(X)$) and is defined by recursion as follows: \end{eqnarray} %%%%%%%%%%%%%%%%%%%%% -\subsection{Recursor} -\subsubsection{Type} +\SubSection{Recursor} +%\SubSubSection{Type} The type of the recursor $\Rx$ on an inductive type $X$ is $$\Rx : \vec{\square\{C(X)\}} \to X \to \alpha$$ $\square$ is defined by recursion on the constructor type $C(X)$. @@ -593,7 +604,7 @@ $\square$ is defined by recursion on the constructor type $C(X)$. \square\{T \to C(X)\} & = & T \to \square\{C(X)\}\nonumber \\ \square\{X \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber \end{eqnarray} -\subsubsection{Reduction rules} +%\SubSubSection{Reduction rules} We say that $$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto \triDOWN\{C(X)_i, f_i, \vec{m}\}$$ @@ -611,7 +622,7 @@ We assume $\Rx~\vec{f}~(c_i~\vec{m})$ is well typed, so in the first case we can omit $\vec{m}$ since it is an empty sequence. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Realizability of the induction principle} +\SubSection{Realizability of the induction principle} Once we have inductive types and their induction principle we want to show that the recursor $\Rx$ realizes $\Xind$, that is that $\Rx$ has type $\sem{\Xind}$ and is in relation $\R$ with $\Xind$. @@ -655,7 +666,7 @@ t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R Q(c_i~\vec{m}~\vec{t})$. \end{proof} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Strong normalization of extended system T} +\Section{Strong normalization of extended system T} Strong normalization for system T is a well know result\cite{GLT} that can be easily extended to System T with this kind of inductive types. The first thing we have to do is to extend the definition of @@ -708,7 +719,7 @@ are straightforward applications of the induction hypothesis. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Improving inductive types} +\Section{Improving inductive types} It is possible to parametrise inductive types over other inductive types without much difficulties since the type $T$ in $C(X)$ is free. Both the recursor and the induction principle are schemas, parametric over $T$. @@ -723,6 +734,9 @@ Se ammettiamo che i tipi dipendano da termini di tipo induttivo %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\bibliographystyle{latex8} +%\bibliography{latex8} + \begin{thebibliography}{} \bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures. Foundations of Computing, Cambrdidge University press, 1991. -- 2.39.2