The Twelf Project

Twelf is a language used to specify, implement, and prove properties of deductive systems such as programming languages and logics. Large research projects using Twelf include the TALT typed assembly language, a foundational proof-carrying-code system, and a type safety proof for Standard ML. Twelf is no longer undergoing active development, but it retains a community of users and remains a valuable tool for research.

Here’s what it looks like to write Twelf:

exp : type.
app : exp -> exp -> exp.
lam : (exp -> exp) -> exp.

step : exp -> exp -> type.
step/app : step (app (lam [x] E0 x) E2) (E0 E2).

Here’s what it looks like to run Twelf:

omega = app (lam [x] app x x) (lam [x] app x x).
%query 1 1 step omega E.

omega : exp = app (lam ([x:exp] app x x)) (lam ([x:exp] app x x)).
%query 1 1
step omega E.
---------- Solution 1 ----------
E = app (lam ([x:exp] app x x)) (lam ([x:exp] app x x)).
____________________________________________
%% OK %%

Visitors without a technical background are encouraged to read the general description of Twelf.

• The installation instructions can get you started.
• Proving metatheorems with Twelf is a mini-course on some of the most common ways of using Twelf.
• The glossary and documentation hub are the most up-to-date documentation for Twelf.

This website is home of Twelf language and the home for lots of Twelf-centric tutorials on logic and programming languages. See the case studies hub for more. Don’t be shy about contributing to our documentation or adding your own tutorials or case studies!

This website is still in the process of being converted from the MediaWiki installation that ran from 2006-2024, and there is much to do. We’d welcome your help!