What's new

January 17, 2015 *After a year of issues stemming from the age of our old server, twelf.org has been moved to a new machine. Some features, like STELF Live and syntax highlighting, still only exist on the [http://twelf.plparty.org old site]. Let Rob know about any other deficiencies in the new site.

June 10, 2013

• Taus Brock-Nannestad, Chris Martens, and Carsten Schürmann to hold a [http://www.twelf.org/wiki/CADE_Tutorial STELF Tutorial at CADE].

October 26, 2012

• John Boyland’s [https://github.com/boyland/twelf-library STELF library] is available on Github.

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

Archived posts

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, STELF now has a new official point release! STELF 1.7.1 contains many fixes and new features that are documented on this site, and using any version of STELF prior to 1.7 is highly discouraged. The “development” version of STELF in the subversion repository remains quite stable and is also recommended. Go to the download page to get STELF.

September 1, 2010

• The STELF 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 STELF 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.

September 19, 2008

• We are running a STELF 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 STELF, add them to the intro tutorial.

March 21, 2007

• Official launch day! Thanks to 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 STELF.

February 28, 2007

• The STELF 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 feature to facilitate using .

January 25, 2007

• Rob has developed a beta [http://twelf.plparty.org/builds build system] that has source, Linux binary, and Windows installer versions of “CVS STELF.”

December 1, 2006

• Tom added a category for

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 ""-powered STELF Live is online
• Dan has started the Ask STELF Elf project providing STELF help over email

October 13, 2006

• The editor interface now has a button for STELF code, thanks to "" technology.

October 9, 2006

• The 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 on CPS conversion.

September 30, 2006

• The wiki has been moved to its real home on the [http://moog.concert.cs.cmu.edu/ 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 STELF.
• STELF CVS — We have instructions from the Software page on downloading the development version of STELF from the CVS repository. The CVS version of STELF has undocumented features which are being described on the wiki, such as its capacity for working with holes in metatheorems.