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.

February 22, 2009

• Rob has a case study on lax logic that uses the admissibility of cut and identity show a sound and complete correspondence between two sequent calculus presentations of lax logic.

October 1, 2008

• Carsten says: As a result of the work of some overly active system administrators at the ITU, the twelf mailing list was accidentally erased a few weeks ago. Since then I have tried to reconstruct the subscriber list with more or less success, but there are still some that I have missed. Therefore, if you haven't received any mail from the list lately, but you expect to be on it, please resubscribe under [http://mail.itu.dk/mailman/listinfo/twelf-list].

September 19, 2008

• We are running a Twelf Tutorial co-located with POPL 2009.

July 19, 2008

• Dan added course materials for the UofO summer school.

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."

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