Directories are organized as follows:
PTT
: This is a formalization of Process Type Theory. Some simplifications have been made on the way, such as binary connectives together with units instead of n-ary connectives. Cut-eliminitation is proved admissible on a particular for of processes where the cuts and tensors are splitting their proof immediately.SendRecv
: This is a formalization of a sub-system which does not haveâ…‹
and⊗
but onlysend
andrecv
.Control.Protocol
: Is a library based onsend
/recv
protocols. Multiplicative connectives (â…‹
and⊗
) are partially emulated.
The HTML highlighted version (not necessarily up to date):
This development requires some extension to the standard libarary:
This development is part of a bigger project: