Verification of programs on truly nested datatypes in intensional type theory
the Coq vernacular file
LNMItMSFP.v
with the implementation
The current version of
LNMItMSFP.v
is 1.3 (June 30, 2006).
There is now (April 15, 2007) a completely
revised version with complete examples
.
Ralph Matthes