Type-Safe Distributed Programming with ML5

  • Tom Murphy VII
  • Karl Crary
  • Robert Harper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4912)


We present ML5, a high level programming language for spatially distributed computing. The language, a variant of ML, allows an entire distributed application to be developed and reasoned about as a unified program. The language supports transparent mobility of any kind of code or data, but its type system, based on modal logic, statically excludes programs that use mobile resources unsafely. The ML5 compiler produces code for all of the hosts that may be involved in the computation. These hosts may be heterogeneous, with different resources and even different architectures. Currently, our compiler and runtime are specialized to the particular case of web programming: a distributed computation with two sites, the web browser and the web server.


Modal Logic Type Representation Type Inference Typing Judgment Document Object Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Appel, A.: Compiling With Continuations. Cambridge University Press, Cambridge (1992)Google Scholar
  2. 2.
    Chong, S., Liu, J., Myers, A.C., Qi, X., Vikram, K., Zheng, L., Zheng, X.: Secure web applications via automatic partitioning. In: 21st ACM Symposium on Operating Systems Principles (SOSP), October 2007 (2007)Google Scholar
  3. 3.
    Cooper, E., Lindley, S., Wadler, P., Yallop, J.: Links: Web programming without tiers. In: de Boer, et al. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 266–296. Springer, Heidelberg (2007)Google Scholar
  4. 4.
    ECMAScript language specification. Technical Report ECMA-262 (1999)Google Scholar
  5. 5.
    Hybrid logics bibliography (2005),
  6. 6.
    W3C DOM IG. Document object model (2005),
  7. 7.
    Jia, L., Walker, D.: Modal proofs as distributed programs (extended abstract). In: European Symposium on Programming (2004)Google Scholar
  8. 8.
    Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge, Massachusetts (1997)Google Scholar
  9. 9.
    Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Transactions on Programming Languages and Systems 21(3), 527–568 (1999)CrossRefGoogle Scholar
  10. 10.
    Murphy VII, T.: The wizard of TILT: Efficient(?), convenient and abstract type representations. Technical Report CMU-CS-02-120, Carnegie Mellon School of Computer Science (2002)Google Scholar
  11. 11.
    Murphy VII, T.: Modal types for mobile code (thesis proposal). Technical Report CMU-CS-06-112, Carnegie Mellon, Pittsburgh, Pennsylvania, USA (2006)Google Scholar
  12. 12.
    Murphy VII, T., Crary, K., Harper, R.: Distributed control flow with classical modal logic. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Murphy VII, T., Crary, K., Harper, R., Pfenning, F.: A symmetric modal lambda calculus for distributed computing. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), IEEE Computer Society Press, Los Alamitos (2004)Google Scholar
  14. 14.
    Park, S.: A modal language for the safety of mobile values. In: Fourth ASIAN Symposium on Programming Languages and Systems, November 2006 (2006)Google Scholar
  15. 15.
    Plainfossé, D., Shapiro, M.: A survey of distributed collection techniques. Technical report, BROADCAST (1994)Google Scholar
  16. 16.
    Schürmann, C., Pfenning, F.: A coverage checking algorithm for LF. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 120–135. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  17. 17.
    Serrano, M., Gallesio, E., Loitsch, F.: HOP, a language for programming the Web 2.0. In: Proceedings of the First Dynamic Languages Symposium (2006)Google Scholar
  18. 18.
    Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh (1994)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Tom Murphy VII
    • 1
  • Karl Crary
    • 1
  • Robert Harper
    • 1
  1. 1.Department of Computer ScienceCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations