Home

The New Twelf Wiki

We are pleased to announce the Twelf Wiki, a major new source of documentation about Twelf:

http://twelf.plparty.org

Twelf is a tool used to specify, implement, and prove properties of deductive systems. The Twelf Wiki includes:

  • A new introduction to LF and Twelf.
  • Tutorials on common Twelf tricks and techniques.
  • Case studies of larger applications of Twelf, including encodings of and proofs about linear logic, mutable state, and CPS conversion.
  • Pre-compiled CVS builds of Twelf for Linux and Windows.

We invite you to come share what you know, learn from what's there, and ask questions about what's not.

- The Twelf Wiki Team

(I know many of the people working on this, and they've put in a lot of effort to make a really useful resource.)

By neelk at 2007-03-21 16:06 | Teaching & Learning | Type Theory | other blogs | 10466 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Wish

I think this is a great thing. One thing that I'd love to see is for Oleg to give some background (here or on the Wiki) as to why, as an avid O'Caml programmer, he and his colleagues chose to use Twelf for their recent proofs, as opposed to, e.g. Coq. I don't mean that to be critical; I'm genuinely curious as to what the relative pros and cons are, and think that someone who's done "real work" using the tool could shed some invaluable light on the subject.

I'd also love to see a compare-and-contrast between some of that real-world Twelf work and, say, Xavier Leroy's compiler work in Coq.

By Paul Snively at Wed, 2007-03-21 18:41 | login or register to post comments

The impression I've had for a while

The impression I've had for a while is that Twelf is more explicitly and intentionally aimed at programming language specification whereas Coq is not intentionally aimed in that area. See e.g. this.

There are also pretty big differences between LF based systems and CoC based systems. I haven't really used Elf/Twelf/etc. or Coq, but my impression from what I've read is that I, personally, would prefer LF based systems, but that doesn't mean that even I would find it better for this particular purpose.

Of course, none of this says anything about what Oleg thinks.

By Derek Elkins at Wed, 2007-03-21 21:20 | login or register to post comments

That's What I Thought Too...

...for the longest time. I kept trying to penetrate MetaPRL because of its explicit focus on programming language design. But then I found an increasing amount of stuff related to PLT in Coq—with Leroy's work admittedly being the most on-point and quite recent—and was forced to reconsider, and ultimately abandon, my quest to master MetaPRL.

It'd be nice, someday, to really get a rundown on how at least a few of these tools, e.g. Twelf, Coq, and Maude, compare in simplifying the formalization of the design of a powerful modern programming language with non-trivial semantics, types, and syntax.

By Paul Snively at Wed, 2007-03-21 22:12 | login or register to post comments

missing a big one

Don't forget Isabelle/HOL.

By Dave Herman at Thu, 2007-03-22 05:52 | login or register to post comments

Rundown

If we could get a really simple example (simply typed lambda calculus?) to be formalised in each of these systems it would do a lot towards giving a feel for how they compare.

By Gavin Mendel-Gleason at Thu, 2007-03-22 10:47 | login or register to post comments

STLC - the "Hello World" of proof assistants

I tracked down examples with Google, so they may not be the best examples.

I don't know that this gives much more intuition about using the systems than a "Hello World" program lets you know how easy it is to program large pieces of software: the ease/clarity with which a small example can be formalized is obviously not necessarily indicative of scalability.

By Rob Simmons at Thu, 2007-03-22 13:45 | login or register to post comments