[MLton] Welcome to Paulo Jorge de Oliveira Cantante de Matos
Stephen Weeks
MLton@mlton.org
Thu, 11 Dec 2003 17:43:06 -0800
I'd like to introduce everyone to Paulo Jorge de Oliveira Cantante de
Matos, who has joined the MLton mailing list. He is interested in
automated theorem proving, Isabelle (maybe porting it to MLton), and
has also looked into a MLton package for Gentoo. His home page is
http://mega.ist.utl.pt/~pocm/
Paulo, back in October 2000, we had a brief discussion with Larry
Paulson about Poly/ML and Isabelle. He had looked into porting it to
MLton, without success, although I don't know how much effort he put
in to it. I also spent a few hours trying to port it at the time, and
decided it would be too much time to completely port. You might like
to look at the "benchmarking Poly/ML" thread at
http://www.mlton.org/pipermail/mlton/2000-October/thread.html
Things might be better these days with hopefully a more consistent
basis library between Poly/ML and MLton. One remaining problem will
be that MLton does not have "use", which was used heavily in Poly/ML.
When I played around with it back in 2000, I was able to eliminate the
uses from the parts I looked at, but it took some work.
Anyways, we'd love to see a port of Isabelle to MLton and would be
happy to help out with any MLton questions you mayhave.