Abstract

In this paper, we study program transformations called useless-code elimination and program slicing in the context of the pi-calculus. The aim of useless-code elimination and program slicing is to simplify a program by eliminating useless or unimportant part of the program. We define formal correctness criteria for those transformations, present a type-based transformation method, and prove its correctness.