
Logic & Semantics 
A process terminates if it does not have an infinite sequence of reductions.
Termination is a useful property in concurrency. For instance, termination may be useful to show that when a given service is interrogated, it will eventually produce an answer. Similarly, a terminating applet, when loaded on a machine, will not run for ever on the machine, possibly absorbing all computing resources (a `denial of service' attack).
We ensure termination of a nontrivial subset of the picalculus by a combination of conditions based on types and on the syntax.
The proof of termination is in two parts. The first uses the technique of logical relation  a wellknow technique of lambdacalculi  on a small set of `functional' processes. The second part of the proof uses techniques of process calculi, in particular techniques of behavioural preorders.