Type coercions for program rewriting

In a joint project between MSR Redmond, Cambridge, and UMD, we have been investigating ways of embedding domain-specific languages within general-purpose languages like ML. Our approach allows DSL designers to design typed APIs to libraries that implement the DSL's features and to provide code to adapt source programs for use with these libraries. Our algorithms take these as specifications and rewrite source programs to use the DSL libraries automatically.

Try Coco! We have built a prototype of our program rewriting approach as a front-end to the OCaml compiler. Our implementation is called "Coco", for "Coercions Compiler". An initial release of Coco together with several example programs is available from here. It is issued under the open source Microsoft Public License (MS-PL).

People

Gavin Bierman (Microsoft Research, Cambridge) 

Nataliya Guts (University of Maryland)

Michael Hicks (University of Maryland)

Daan Leijen (Microsoft Research, Redmond)

Nikhil Swamy (Microsoft Research, Redmond)

 

Publications

Nikhil Swamy, Nataliya Guts, Daan Leijen, and Michael Hicks, Lightweight Monadic Programming in ML, in Proceedings of the International Conference on Functional Programming, Association for Computing Machinery, Inc., 2011

Nikhil Swamy, Michael Hicks, and Gavin Bierman, A Theory of Typed Coercions and its Applications, in Proceedings of the International Conference on Functional Programming, Association for Computing Machinery, Inc., 8 June 2009