[MLton] Re: refinement type checker for Standard ML

[Frank Pfenning]

Hi Stephen,

  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 <rowan@cs.uwa.edu.au>, 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.

  - Frank

> Date:    Wed, 7 Jan 2004 09:16:28 -0800
> To:      Frank Pfenning <fp@cs.cmu.edu>
> CC:      MLton@mlton.org
> From:    Stephen Weeks <sweeks@sweeks.com>
> 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
> 
> 	http://www.mlton.org/experimental/
> 
> 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.