Verification of programs on truly nested datatypes in intensional type theory

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