What's new
From The Twelf Project
- 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
- 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."
[edit] Archived posts
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.
