What's new

From The Twelf Project

September 2, 2011

• We've finally moved from twelf.plparty.org to twelf.org! All old links will continue to work through at least August 2013 (and they should actually continue to work indefinitely).

March 19, 2011

• After many years of new features being added only to the subversion branch, Twelf now has a new official point release! Twelf 1.7.1 contains many fixes and new features that are documented on this site, and using any version of Twelf prior to 1.7 is highly discouraged. The "development" version of Twelf in the subversion repository remains quite stable and is also recommended. Go to the download page to get Twelf.

September 1, 2010

• The Twelf Wiki has undergone an upgrade, and in the process code underlying the syntax-highlighing TwelfTag system has been substantially rewritten and simplified. However, this meant several deprecated-but-still-used options to the <twelf> tags now don't work and print error messages. Leave a note on Rob's talk page if you see any weird error messages around Twelf code.

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

[edit] Archived posts

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 16, 2007

• Dan has revised and expanded several of the tutorials, and written new ones on catch-all cases, numeric termination metrics, and hereditary substitution.

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

October 30, 2006

• Tom posted a case study on Admissibility of cut.

October 20, 2006

• Jake posted a tutorial on Strengthening.

October 19, 2006

• Carsten is developing a case study on lists.

October 18, 2006

• Tom posted a case study for Classical S5.

October 16, 2006

• Karl posted a case study on Linear logic.

October 14, 2006

• An alpha version of "AJALF"-powered Twelf Live is online
• Dan has started the Ask Twelf Elf project providing Twelf help over email

October 13, 2006

• The editor interface now has a quick check button for Twelf code, thanks to "AJALF" technology.

October 9, 2006

• The TwelfTag system now allows for direct checking of code in the wiki.
• Carsten has added code proving various properties of Lily to the case studies.

October 5, 2006

• Tom posted an advanced tutorial on CPS conversion.

September 30, 2006

• The wiki has been moved to its real home on the Moog server, and given a permanent domain name, twelf.plparty.org.
• A first draft of the non-technical quick introduction has been introduced for consideration.

September 28, 2006

• Substitution lemma — Dan Lee's thorough explanation of the different ways substitution lemmas are dealt with by Twelf.
• Twelf CVS — We have instructions from the Software page on downloading the development version of Twelf from the CVS repository. The CVS version of Twelf has undocumented features which are being described on the wiki, such as its capacity for working with holes in metatheorems.