Lambda the Ultimate

TyPiCal is a type-based static analyzer for the pi-calculus. The current version of TyPiCal provides four kinds of program analyses or program transformations: lock-freedom analysis, deadlock-freedom analysis, useless-code elimination, and information flow analysis.

Type system is an ordinary type system extended so that channel types carry precise information about how each channel is used. This allows a type inferencer to obtain information about the behavior of a process.