Using Twelf

While learning to use Twelf, I wrote an under-informed and biased tutorial (PDF) on using Twelf to prove type theorems. This tutorial is over 3 years old (in late 2010) and should be updated to be a better introduction.

More importantly, I implemented library “signatures”. To make up for a lack of a module system, some of these signatures are produced through use of the C preprocessor. I also fake a module system, using backquote ` since . is (correctly) not legal in a name.

All of these signatures (in one compressed tar) and sources of generated ELF code are offered without restriction to anyone who wishes to use them in any way. (Last update: November 27, 2010.)
Using Twelf / boyland@cs.uwm.edu