Abstract
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.
The ConCert Project is supported by the National Science Foundation under grant ITR/SY+SI 0121633: “Language Technology for Trustless Software Dissemination.”
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Appel, A.: Compiling With Continuations. Cambridge University Press, Cambridge (1992)
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)
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)
ECMAScript language specification. Technical Report ECMA-262 (1999)
Hybrid logics bibliography (2005), http://hylo.loria.fr/content/papers.php
W3C DOM IG. Document object model (2005), http://w3c.org/DOM/
Jia, L., Walker, D.: Modal proofs as distributed programs (extended abstract). In: European Symposium on Programming (2004)
Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge, Massachusetts (1997)
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)
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)
Murphy VII, T.: Modal types for mobile code (thesis proposal). Technical Report CMU-CS-06-112, Carnegie Mellon, Pittsburgh, Pennsylvania, USA (2006)
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)
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)
Park, S.: A modal language for the safety of mobile values. In: Fourth ASIAN Symposium on Programming Languages and Systems, November 2006 (2006)
Plainfossé, D., Shapiro, M.: A survey of distributed collection techniques. Technical report, BROADCAST (1994)
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)
Serrano, M., Gallesio, E., Loitsch, F.: HOP, a language for programming the Web 2.0. In: Proceedings of the First Dynamic Languages Symposium (2006)
Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Murphy VII, T., Crary, K., Harper, R. (2008). Type-Safe Distributed Programming with ML5. In: Barthe, G., Fournet, C. (eds) Trustworthy Global Computing. TGC 2007. Lecture Notes in Computer Science, vol 4912. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78663-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-78663-4_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78662-7
Online ISBN: 978-3-540-78663-4
eBook Packages: Computer ScienceComputer Science (R0)