Substructural Meta-Theory of a Type-Safe Language forWeb Programming

• Autorzy: Cervesato I. , Sans T.

Identyfikatory

DOI

10.3233/FI-2014-982

• Języki publikacji: EN

Abstrakty

EN

This paper introduces an abstract web programming language, QWeSST, and a methodology for proving properties of formalisms, such are QWeSST, that are parallel, distributed and concurrent. At its core, QWeSST is a small functional programming language extended with primitives for mobile code and remote procedure calls, two distinguishing features of web programming. It supports a localized view of typechecking and of evaluation, which reflects the way we program web applications and web services. We have developed a prototype implementation for QWeSST and used it to elegantly write simple web applications that are however not easily expressed using current web technology. We give two semantics for QWeSST, one is standard and models a naive form of single-threaded evaluation, the other is maximally parallel and exploits a presentation of its typing and execution behaviors based on an extended form of substructural operational semantics. It augments standard inference rules with a construction that realizes parametric multiset comprehension, which makes it convenient to capture ensemble-level behaviors. We prove that both semantics are type safe, the former using traditional methods, the latter by developing a proof methodology that parallels the multiset-oriented presentation of the semantics.

Słowa kluczowe

EN

web programming; type safety; parallelism; mobile code; substructural operational semantics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 130, nr 1
• Strony: 67--97
• Opis fizyczny: Bibliogr. 33 poz., rys.

Twórcy

autor

Cervesato I.

• Carnegie Mellon University, Qatar

autor

Sans T.

• Carnegie Mellon University, Qatar

Bibliografia

• [1] Baldoni, M., Baroglio, C., Martelli, A., Patti, V.: A priori conformance verification for guaranteeing interoperability in open environments, Proc. 4th International Conference on Service Oriented Computing (ICSOC’06) (A. Dan, W. Lamersdorf, Eds.), Springer-Verlag LNCS 4294, Chicago, IL, 2006.
• [2] Brown, L., Sahlin, D.: Extending Erlang for Safe Mobile Code Execution, Proceedings of the 2nd International conference on Information and Communication Security, Sydney, Australia, 1999.
• [3] Cardelli, L., Gordon, A. D.: Anytime, anywhere. Modal logics for mobile ambients, Proceedings of the 27th Symposium on Principles of Programming Languages (POPL’00), ACM Press, San Antonio, TX, 2000.
• [4] Cervesato, I., Pfenning, F., Walker, D., Watkins, K.: A Concurrent Logical Framework II: Examples and Applications, Technical Report CMU-CS-02-102, Carnegie Mellon University, Pittsburgh, PA, 2003.
• [5] Chong, S., Liu, J., Myers, A. C., Qi, X., Vikram, K., Zheng, L., Zheng, X.: Secure web applications via automatic partitioning, Proceedings of the 21st ACM Symposium on Operating Systems Principles (SOSP’07), Stevenson, WA, 2007.
• [6] Cooper, E., Lindley, S., Wadler, P., Yallop, J.: Links: Web Programming Without Tiers, Formal Methods for Components and Objects, 2007, 266–296.
• [7] Cooper, E.,Wadler, P.: The RPC Calculus, Proceedings of the 11th Symposium on Principles and Practice of Declarative Programming — PPDP’09 (A. Porto, F. L´opez-Fraguas, Eds.), ACM, Coimbra, Portugal, 2009.
• [8] De Labey, S., van Dooren, M., Steegmans, E.: ServiceJ A Java Extension for Programming Web Services Interactions, Web Services, 2007. ICWS 2007. IEEE International Conference on, 2007.
• [9] El-Ansary, S., Grolaux, D., Roy, P. V., Rafea, M.: Overcoming the multiplicity of languages and technologies for web-based development using a multi-paradigm approach, Procceedings of the 2nd International Conference on Multiparadigm Programming in Mozart/Oz (MOZ’04), 2004.
• [10] Ellison III, C. M.: A Rewriting Logic Approach to Defining Type Systems, Master Thesis, University of Illinois at Urbana-Champaign, 2008.
• [11] Ellison III, C. M., S¸ erb˘anut¸˘a, T. F., Ros¸u, G.: A Rewriting Approach to Type Inference, Technical Report UIUCDCS-R-2008-2934, University of Illinois at Urbana-Champaign, 2008.
• [12] Ferrara, A.: Web services: a process algebra approach, ICSOC ’04: Proceedings of the 2nd international conference on Service oriented computing, ACM, New York, NY, USA, 2004.
• [13] Google Inc.: Google Web Toolkit, http://code.google.com/webtoolkit/.
• [14] Jia, L., Walker, D.: Modal Proofs as Distributed Programs, Programming Languages and Systems, 2004, 219–233.
• [15] Mandel, L., Maranget, L.: Programming in JoCaml, Technical Report RR-6261, MOSCOVA – INRIA Rocquencourt, 2007.
• [16] Murphy VII, T.: Modal Types for Mobile Code, Ph.D. Thesis, Carnegie Mellon University, January 2008, Available as technical report CMU-CS-08-126.
• [17] Murphy VII, T., Crary, K., Harper, R.: Type-Safe Distributed Programming with ML5, Trustworthy Global Computing, 2008, 108–123.
• [18] Pfenning, F.: Substructural Operational Semantics and Linear Destination-Passing Style, 2004, Invited talk to the Second Asian Symposium on Programming Languages and Semantics (APLAS’04). Slides at http://www.cs.cmu.edu/~fp/talks/aplas04-talk.ps.
• [19] Pfenning, F., Sch¨urmann, C.: System Description: Twelf — A Meta-Logical Framework for Deductive Systems, Proc. CADE-16 (H. Ganzinger, Ed.), Springer-Verlag LNAI 1632, Trento, Italy, 1999.
• [20] Pfenning, F., Simmons, R. J.: Substructural Operational Semantics as Ordered Logic Programming, Proc. 24th IEEE Symposium on Logic in Computer Science—LICS’09, Los Angeles, CA, 2009.
• [21] Qwel —programming language for the web, http://qwel.qatar.cmu.edu.
• [22] Reppy, J.: Concurrent Programming in ML, Cambridge University Press, 1999.
• [23] Rossberg, A.: Typed Open Programming - A higher-order, typed approach to dynamic modularity and distribution, Ph.D. Thesis, Universit¨at des Saarlandes, 2007.
• [24] Rossberg, A., Botlan, D. L., Tack, G., Brunklaus, T., Smolka, G.: Alice through the looking glass, Proceedings of the 4th Symposium on Trends in Functional Programming (TFP’04), Intellect Books, Munich, Germany, 2004.
• [25] Sangiorgi, D., Walker, D.: The _-Calculus: a Theory of Mobile Processes, Cambridge University Press, 2001.
• [26] Sans, T., Cervesato, I.: QWeSST for Type-SafeWeb Programming, Third International Workshop on Logics, Agents, and Mobility — LAM’10 (B. Farwer, Ed.), Edinburgh, Scotland, UK, 2010.
• [27] Sans, T., Cervesato, I.: Type-Safe Web Programming in QWeSST, Technical Report CMU-CS-10-125, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, June 2010.
• [28] Schack-Nielsen, A., Sch¨urmann, C.: Celf—a logical framework for deductive and concurrent systems (system description), Proceeding of IJCAR’08, Springer-Verlag LNCS 5195, 2008.
• [29] Serrano, M., Gallesio, E., Loitsch, F.: Hop, a Language for Programming the Web 2.0, Proceedings of the First Dynamic Languages Symposium (DLS’06), Portland, OR, 2006.
• [30] Simmons, R. J.: Type safety for substructural specifications: preliminary results, Technical Report CMUCS-10-134, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, July 2010.
• [31] The Twelf project wiki, http://twelf.org.
• [32] Unypoth, A., Sewell, P.: Nomadic Pict: Correct communication infrastructure for mobile computation, Proc. 28th ACM Symposium on Principles of Programming Languages (POPL’01), London, UK, 2001.
• [33] World Wide Web Consortium (W3C): Web Services Description Language (WSDL), 2007.