[MLton] Welcome to Paulo Jorge de Oliveira Cantante de Matos

Paulo Jorge de Oliveira Cantante de Matos pocm@netvisao.pt
Mon, 15 Dec 2003 01:05:50 +0000


Dear all,

First of all, I'd like to thank Stephen for his warm welcome and I'd
like to say that I'm just starting to work with MLton and SML at all so
I think I'll have a lot of time ahead of me to work in to it.

I've created a MLton binary ebuild for Gentoo GNU/Linux, which will be
available tomorrow at my homepage, if anyone is interested. I've also
send a enhancement report for Gentoo bug tracking system so that they
had the ebuild to portage (their base package system).

I'm working in Automated Theorem Prover, trying to integrate NuPRL5 and
Isabelle and I hope to be able to port Isabelle to MLton. 

Well, I think it's all for now. I'll just post a question to the user
mailing list. ;) And when I have some deeper questions regarding MLton
I'll post here. 

Oh, I was about to forget... My personal email is pocm at
mega.ist.utl.pt. This one pocm at netvisao.pt is only used for mailing
list archiving. If you want to contact me please send the email to the
former address.

Thanks you all once again,

Best Regards,

Paulo Matos


On Fri, 2003-12-12 at 01:43, Stephen Weeks wrote:
> 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.
> 
> _______________________________________________
> MLton mailing list
> MLton@mlton.org
> http://www.mlton.org/mailman/listinfo/mlton
-- 

Paulo J. Matos : pocm [_at_] mega . ist . utl . pt
Instituto Superior Tecnico - Lisbon
Computer and Software Eng. - A.I.
 - > http://mega.ist.utl.pt/~pocm
---
        -> God had a deadline...
                So, he wrote it all in Lisp!