--------------------------------------------------------
Coding of the pi-calculus in COQ
--------------------------------------------------------

author : Loic Henry-Greard
email  : [email protected]
www    : http://www.inria.fr/meije/personnel/Loic.Henry-Greard/index.html

These files contain 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,
LFCS report 1997
http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/97/ECS-LFCS-97-359/index.html

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.

A Makefile is included, generated by COQ's do_Makefile command.
typical targets are:

make all 

	to build all the .vo files

make clean
	
	to delete all generated files and start afresh
        a new compiling with e.g. different dependencies.

make depend

	to recompute dependencies using COQ's coqdep command
	in the .depend file.

a complete description and discussion of that coding can be found
on my web page.