Main Page

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

Learn Twelf:

• Read the introductions to Twelf first.
• The tutorials explain common Twelf tricks and techniques.
• The case studies present interesting applications of Twelf.
• The glossary defines Twelf terminology.
• Have a question? Ask Twelf Elf!

See the documentation page for more resources.

January 28, 2008

• John took Rob's example to the next step and directly provided a bijection between a HOAS encoding of lambdas and natural numbers.

October 4, 2007

• Rob posted a page on concrete representation based on a question by John about demonstrating a correspondence between HOAS and concrete term representations.

April 25, 2007

• Todd posted a tutorial on using Church encodings to create user-defined constraint domains.

April 11, 2007

• If you think up some exercises while you're learning Twelf, add them to the intro tutorial.

March 21, 2007

• Official launch day! Thanks to everyone who has contributed so far, and welcome to new visitors.

March 14, 2007

• Dan has finished a draft of the introductory article Proving metatheorems with Twelf.

February 28, 2007

• The Twelf Project wiki now supports uploading SVG images! Check out the article on tabled logic programming for an example of the unnecessarily beautiful illustrations this allows.

February 24, 2007

• Rob has extended the TwelfTag feature to facilitate using Literate Twelf.

January 25, 2007

• Rob has developed a beta build system that has source, Linux binary, and Windows installer versions of "CVS Twelf."

December 1, 2006

• Tom added a category for undocumented features

To read about older updates, see the What's new? page.