[MLton-devel] Re: Twelf benchmark

[Frank Pfenning]

It depends on which verson of Twelf you are using.

We now have large developments in Twelf.  Andrew Appel has about
100K lines of Twelf source formalizating foundational PCC, and test
suites that run between minutes and hours.

Karl Crary has a formalization of Typed Assembly Language in Twelf
that runs about a minute.

Both of these require relatively recent features of Twelf.

It is also easy to make up artifical examples that run very slowly
using older versions of Twelf.

By the way, I would be interested in maintaining the Twelf source
in a manner so that it can be compiled under MLton as well as
SML/NJ.  Do you have a suggestion for the best way to do this?

  - Frank


-------------------------------------------------------
This sf.net email is sponsored by:
With Great Power, Comes Great Responsibility 
Learn to use your power at OSDN's High Performance Computing Channel
http://hpc.devchannel.org/
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel