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.

- Some simple definitions that
*should*be standard.std.elf (The name is an overreach!)

- Boolean constants. This includes some standard equality and inequality theorems (such as the transitivity of equality) that I try to prove for all data types.
- Natural numbers (composed using
`z`and`s`). The signature includes`plus`,`times`,`eq`,`gt`(greater than), and a number of other mainly derived relations (`minus`,`ge`,`lt`etc). It also includes a`divrem`operation for integer division with remainder. The package includes over 300 theorems about these relations all with automatically-checked hand-written proofs (using Twelf 1.5R3). - Pairs. This trivial "functor" of pairs. There is an
instantiation for pairs of natural numbers that includes
an isomorphism from pairs to natural numbers, so that pairs
can be (indirectly) used as keys to maps (q.v.).
pair.elf (the functor), natpair.elf (pairs of natural numbers).

- Positive rational numbers (represented using continued fractions).
The signature requires “nat.elf” and "natpair.elf"
and includes
`add`,`mul`,`equ`,`grt`and derived relations, including similar relations as above, but also a`div`relation. Division is a total operation over the positive rationals. The signature includes an isomorphism from positive rationals to the natural numbers which enables rational numbers to serve as the domain of a map (q.v.). The package includes well over 300 fully-proved theorems. - Partial maps. This signature represents maps from natural
numbers to an unspecified datatype
`data`. It must be customized before use. It includes over 55 fully-proved theorems. Additionally, if the "data" datatype supports leq,join and/or meet operations, there are definitions of these operations for maps and over 100 extra theorems involving them.map.elf (the signature, hand-written), map.tgz (all of the map theorems).

- Sets of natural numbers. This signature implements finite sets
of natural numbers. As above, the representation is "adequate":
two sets are equivalent iff they are equal. The signature
is mainly generated by instantiating the "map" "functor"
with "data" being "unit". Among other operations are
`member`,`not-member`,`leq`,`union`,`intersection`,`add`(single element) and`remove`(sets). The signature includes well over 300 fully proved theorems about these operations. - Multisets of natural numbers. This signature implements
multisets as maps to natural numbers. The
`union`operation does an `max' operation. It is implemented using that`map`"functor." - Vectors (with length). This is a "functor" over a type
with both "add" an "mul" operations defined. The length is used
to ensure there is no attempt made to compare (eq), add or dot
vectors of different length. The "dot" operation is provided
only if the underlying data type includes a zero.
vector.elf (the functor), rat0vector.elf (vectors of non-negative rational numbers).

Using Twelf / boyland@cs.uwm.edu