[MLton] Re: refinement type checker for Standard ML
Frank Pfenning <email@example.com>
Wed, 07 Jan 2004 12:39:51 -0500
yes, we have a "working" refinement checker for SML, modified from
the Kit compiler front end. If you are interested in playing with this,
I could give you read-access to our CVS repository. The author
is Rowan Davies <firstname.lastname@example.org>, so we would need his permission.
Unfortunately, there isn't much documentation, but there are some examples...
Thanks also for the pointer to the experimental MLton. Quite
a few people seem to be using the standalone Twelf server compiled
under MLton. Personally, I won't have much time to think about this
or work on it until the end of February, but I'll see if I can get
a local volunteer.
> Date: Wed, 7 Jan 2004 09:16:28 -0800
> To: Frank Pfenning <email@example.com>
> CC: MLton@mlton.org
> From: Stephen Weeks <firstname.lastname@example.org>
> Subject: refinement type checker for Standard ML
> Hi Frank. A while back you mentioned that you were building a
> refinement type checker for SML. I was curious to hear the status of
> the project. You also mentioned you were interested if MLton had a
> reasonable front end, which at the time it did not. I wanted to let
> you know that we finally have a version of MLton with a proper front
> end. We have an experimental version at
> We are seeking feedback on the new front end, and would appreciate any
> you might be able to provide. It would be especially nice if you or a
> student could try out Twelf on the new MLton. Thanks.