Next:
Tools
Up:
Contents
Previous:
Literature
Example proof developments
Some Lambda Calculus and Type Theory Formalized
(described in a paper to appear in JAR)
Imperative Programs
PhD Thesis 1998
TAPSOFT'97
Program Specification using LEGO
(compressed tar of directory)
Miscellaneous examples
(compressed tar of directory)