1: \documentclass{LMCS}

2: 

3: \usepackage{mathlig,url,amssymb,latexsym,proof,myproof,bcprules,graphicx,hyperref}

4: 

5: \newif \iffull \fulltrue

6: \newif \ifdraft \drafttrue

7: \newif \iftwocol \twocolfalse

8: 

9: \def\Infax{\infax}

10: \def\Infrule{\infrule}

11: 

12: \newlength\figwidth

13: \setlength{\figwidth}{\textwidth}

14: \newlength\hfigwidth

15: \setlength{\hfigwidth}{8cm}

16: 

17: % polarities of channels

18: \input{local}

19: \def\finish#1{\ifdraft {\em [*** #1 ***]} \iffull \marginpar{\huge $*$} \fi

20:   \else \typeout{****FINISH****}\fi}

21: 

22: \raggedbottom

23: %%\overfullrule=2 pt

24: 

25: \def\doi{2 (3:4) 2006}

26: \lmcsheading%

27: {\doi}

28: {1--42}

29: {}

30: {}

31: {Jan.~25, 2006}

32: {Sep.~13, 2006}

33: {}

34: \begin{document}

35: 

36: 

37: 

38: \title[Resource Usage Analysis for the \(\pi\)-Calculus]{Resource Usage Analysis for the $\pi$-Calculus\rsuper*}

39: 

40: %% \and Lucian Wischik

41: % \authorinfo{Naoki Kobayashi

42: % \and Kohei Suenaga

43: % }

44: % \authorinfo{Naoki Kobayashi}{Tohoku University}{koba@ecei.tohoku.ac.jp}

45: % \authorinfo{Kohei Suenaga}{University of Tokyo}{kohei@yl.is.s.u-tokyo.ac.jp}

46: % \authorinfo{Lucian Wischik}{Microsoft Corporation}{lwischik@microsoft.com}

47: \author[N.~Kobayashi]{Naoki Kobayashi\rsuper a}

48: \address{{\lsuper a}6-3-09, Aoba, Aramaki-aza, Aoba-ku, Sendai, Miyagi, Japan}

49: \email{koba@ecei.tohoku.ac.jp}

50: 

51: \author[K.~Suenaga]{Kohei Suenaga\rsuper b}

52: \address{{\lsuper b}6-3-09, Aoba, Aramaki-aza, Aoba-ku, Sendai, Miyagi, Japan}

53: \email{kohei@yl.is.s.u-tokyo.ac.jp}

54: 

55: \author[L.~Wischik]{Lucian Wischik\rsuper c}

56: \address{{\lsuper c}1 Microsoft Way, Redmond, WA 98052, USA}

57: \email{lwischik@microsoft.com}

58: 

59: \keywords{Type System, $\pi$-Calculus, Verification of Concurrent

60: Programs, Resource Usage Analysis}

61: \subjclass{D.2.4, D.3.1, F.3.1, F.3.2}

62: 

63: \titlecomment{{\lsuper *}A preliminary version appeared in 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2006), Charleston, SC, USA, January 8--10, 2006}

64: 

65: \input{Abstract}

66: 

67: \maketitle

68: 

69: % \category{Categories will}{come}{here}

70: % \terms Term comes here

71: % \keywords Keyword comes here

72: 

73: % \newpage

74: % \input{revision}

75: % \newpage

76: \input{Intro}

77: \input{Process}

78: \input{Typing}

79: \input{Soundness}

80: \input{Inference}

81: \input{Extension}

82: \input{Implementation}

83: \input{Related}

84: \input{Conc}

85: %\input{Ack}

86: \bibliographystyle{abbrv}

87: \bibliography{full,koba}

88: \newpage

89: \appendix

90: \section*{Appendix}

91: \input{ProofSubtyping}

92: \input{ProofSubjectReduction}

93: \input{ProofPartialLiveness}

94: %%%\input{AlgorithmPT}

95: \input{Basis}

96: %%%\input{ExamplePrograms}

97: \end{document}

98: