package coq-param-pi

This development contains the specification for a monadic pi-calculus using the same coding method for names than J. Mc Kinna and R. Pollack used for PTS in LEGO: "Some Lambda Calculus and Type Theory Formalized".

The basic, monadic calculus encoded here has a type system restraining the direction of communication for processes' names.

A number of lemmas usefull for doing proofs on that coding are included, and subject reduction properties for each kind of transition is made as an example of actually using the coding to mechanize proofs on the pi-calculus.