1: \section{Conclusion}

2: \label{sec:conclusion}

3: 

4: We have formalized a type system for resource usage analysis

5: and proved its soundness. We have also developed a sound (but incomplete

6: because of the last phase for deciding the trace inclusion relation

7: \(\traces{x}{A}\subseteq \spec\)) algorithm for it

8: in order to liberate programmers from the burden of writing complex type annotations.

9: We have also implemented a prototype resource usage analyzer based on the algorithm.

10: 

11: There remains much future work.

12: It is necessary to assess the effectiveness of our analysis, including

13: the design of the type system and the algorithm for deciding the trace inclusion relation

14: \(\traces{x}{A}\subseteq \spec\), in more detail, and refine the analysis if necessary.

15: It is also necessary to make the analyzer more user-friendly, by devising a method

16: for generating comprehensive explanation of the verification result; currently, the analyzer

17: gives only a yes/no answer.

18: Extensions of the type system to deal with

19: other typical synchronization primitives like join-patterns and internal choice is also

20: left for future work.

21: