[TYPES] Announcement: A Type-Based Analyzer for the Pi-Calculus

[kobayasi at kb.cs.titech.ac.jp]

We would like to announce availability of the first implementation of
TyPiCal: a type-based static analyzer for the pi-calculus.
TyPiCal is based on a series of our work on type systems for
the pi-calculus (some of which are listed below), and can 
perform the following analyses and transformations for pi-calculus processes.

 - Lock-freedom analysis [1], which finds communications that
   will eventually succeed, without suffering from deadlocks, livelocks, etc.

 - Deadlock-freedom analysis [2], which finds communications that
   will eventually succeed unless the whole process diverges

 - Useless-code elimination [3], which eliminates communications that
   do not affect the observable behavior of the process

 - Information flow analysis [4], which finds values whose information
   is kept secret to the environment.

All the analyses and transformation above are fully automatic (no type
annotation is required), thanks to the recent result [4].

TyPiCal is available from:
  
   http://www.kb.cs.titech.ac.jp/~kobayasi/typical/


References
=========
  [1] Naoki Kobayashi, "A Type System for Lock-Free Processes,"
      Information and Computation 177(2), pp.122-159, 2002

  [2] Naoki Kobayashi, Shin Saito, and Eijiro Sumii,
      "An Implicitly-Typed Deadlock-Free Process Calculus,"
      Proceedings of CONCUR 2000, Springer LNCS1877, pp.489-503, 2000

  [3] Naoki Kobayashi, 
      "Useless-Code Elimination and Program Slicing for the Pi-Calculus,"
      Proceedings of The First Asian Symposium on Programming Languages and Systems (APLAS'03)
      Springer LNCS 2895, 2003.

  [4] Naoki Kobayashi, "Type-Based Information Flow Analysis for the Pi-Calculus,"
      Technical Report TR03-0007, Department of Computer Science, 
      Tokyo Institute of Technology, 2003

Best regards,

Naoki Kobayashi
Department of Computer Science
Graduate School of Information Science and Engineering
Tokyo Institute of Technology
2-12-1 Oookayama, Meguro-ku, 
Tokyo 152-8552, Japan
e-mail:kobayasi at cs.titech.ac.jp