Thesis proposal: implement the ML module system from "F-ing modules"

[Blaisorblade]

Since ML modules can be compiled to F, all PTSs that "include" F can support a module system as "syntactic sugar". Some student could do it.

Benefits:

1. a powerful module system for PTS
2. it could allow experimenting with F-ing translation in practice
3. in particular, we should get an implementation of ML modules on top of dependent types.

Downsides:

1. who cares?

[Toxaris]

For reference, Paolo is talking about implementing this paper:

http://www.mpi-sws.org/~rossberg/f-ing/

[Blaisorblade]

BTW, finally Andreas Rossberg did it himself. No reason we can't do it in a thesis for PTS though — but we might reconsider the goals.

http://www.mpi-sws.org/~rossberg/1ml/1ml.pdf http://lambda-the-ultimate.org/node/5121