skip to main content
research-article
Open access

Reasoning about Web Applications: An Operational Semantics for HOP

Published: 01 June 2012 Publication History

Abstract

We propose a small-step operational semantics to support reasoning about Web applications written in the multitier language HOP. The semantics covers both server side and client side computations, as well as their interactions, and includes creation of Web services, distributed client-server communications, concurrent evaluation of service requests at server side, elaboration of HTML documents, DOM operations, evaluation of script nodes in HTML documents and actions from HTML pages at client side. We also model the browser same origin policy (SOP) in the semantics. We propose a safety property by which programs do not get stuck due to a violation of the SOP and a type system to enforce it.

References

[1]
Berry, G. and Boudol, G. 1990. The chemical abstract machine. In Proceedings of the ACM International Conference on Principle of Programming Languages. ACM Press, New York, 81--94.
[2]
Bohannon, A. and Pierce, B. C. 2010. Featherweight Firefox: Formalizing the core of a web browser. In Proceedings of the Usenix Conference on Web Application Development. USENIX Association, Berkeley, CA.
[3]
Boudol, G., Luo, Z., Rezk, T., and Serrano, M. 2010. Towards reasoning for web applications: An operational semantics for hop. In Proceedings of the Workshop on Analysis and Programming Languages for Web Applications and Cloud Applications (APLWACA’10). ACM, New York, NY, 3--14.
[4]
Chlipala, A. 2010. Ur: Statically-typed metaprogramming with type-level record computation. In Proceedings of the International Conference on Programming Languages and Implementation. ACM.
[5]
Chong, S., Liu, J., Myers, A., Qi, X., Vikram, K., Zheng, L., and Zheng, X. 2009. Building secure web applications with automatic partitioning. Comm. ACM 52, 2, 79--87.
[6]
Cooper, E., Lindley, S., Wadler, P., and Yallop, J. 2006. Links: Web programming without tiers. In Proceedings of the 5th International Symposium on Formal Methods for Components and Objects. Springer.
[7]
Cooper, E. E. and Wadler, P. 2009. The rpc calculus. In Proceedings of the 11th ACM SIGPLAN conference on Principles and Practice of Declarative Programming (PPDP’09). ACM, New York, NY, 231--242.
[8]
Felleisen, M. and Hieb, R. 1992. The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103, 2, 235--271.
[9]
Gardner, P., Smith, G., Wheelhouse, M., and Zarfaty, U. 2008a. DOM: Towards a formal specification. In Proceedings of the ACM SIGPLAN Workshop on Programming Language Technologies for XML (PLAN-X). ACM Press.
[10]
Gardner, P., Smith, G., Wheelhouse, M., and Zarfaty, U. 2008b. Local Hoare reasoning about DOM. In Proceedings of the 27th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems. ACM Press, 261--270.
[11]
Graunke, P., Findler, R. B., Krishnamurthi, S., and Felleisen, M. 2003. Modeling web interactions. In Proceedings of the European Symposium on Programming. Springer.
[12]
Guha, A., Saftoiu, C., and Krishnamurthy, S. 2010. The essence of JavaScript. In Proceedings of the 24th European Conference on Object-Oriented Programming. Springer.
[13]
Hors, A. L., Hegaret, P. L., Nicol, G., Robie, J., Champion, M., and Byrne, S. 2000. Document Object Model (DOM) level 2 core specification. Tech. rep., W3C.
[14]
Kelsey, R., Clinger, W. D., and Rees, J. 1998. Revised report on the algorithmic language scheme. SIGPLAN Not. 33, 9, 26--76.
[15]
Loitsch, F. and Serrano, M. 2008. HOP Client-side compilation. In Trends in Functional Programming. Vol. 8, M. T. Morazán Ed., Intellect Bristol, UK, 141--158.
[16]
Maffeis, S., Mitchell, J., and Taly, A. 2008. An operational semantics for JavaScript. In Proceedings of the Asian Symposium on Programming Languages and Systems. Springer.
[17]
Matthews, J., Findler, R. B., Graunke, P. T., Krishnamurthi, S., and Felleisen, M. 2004. Automatically restructuring programs for the web. Autom. Softw. Engin. 11, 4, 337--364.
[18]
Queinnec, C. 2000. The inuence of browsers on evaluators. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming. ACM, 23--33.
[19]
Serrano, M. 2009. HOP, a fast server for the di_use web. In Proceedings of the 11th International Conference on Coordination Models and Languages. Lecture Notes in Computer Science, vol. 5521, Springer 1--26.
[20]
Serrano, M., Gallesio, E., and Loitsch, F. 2006. HOP, a language for programming the web 2.0. In Proceedings of the 1st Dynamic Languages Symposium. ACM, New York, NY.
[21]
Serrano, M. and Queinnec, C. 2010. A multi-tier semantics for HOP. In Higher Order and Symbolic Computation.
[22]
Wright, A. K. and Felleisen, M. 1994. A syntactic approach to type soundness. Inf. Comput. 115, 1, 38--94.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems
ACM Transactions on Programming Languages and Systems  Volume 34, Issue 2
June 2012
212 pages
ISSN:0164-0925
EISSN:1558-4593
DOI:10.1145/2220365
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 June 2012
Accepted: 01 March 2012
Revised: 01 August 2011
Received: 01 December 2010
Published in TOPLAS Volume 34, Issue 2

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Multitier languages
  2. Web programming
  3. functional languages

Qualifiers

  • Research-article
  • Research
  • Refereed

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)60
  • Downloads (Last 6 weeks)10
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2022)Statically identifying XSS using deep learningScience of Computer Programming10.1016/j.scico.2022.102810219(102810)Online publication date: Jul-2022
  • (2022)Varda: A Framework for Compositional Distributed ProgrammingNetworked Systems10.1007/978-3-031-17436-0_2(16-30)Online publication date: 17-May-2022
  • (2020)A Survey of Multitier ProgrammingACM Computing Surveys10.1145/339749553:4(1-35)Online publication date: 26-Sep-2020
  • (2019)A theory of RPC calculi for client–server modelJournal of Functional Programming10.1017/S095679681900002929Online publication date: 22-Mar-2019
  • (2018)Tierless Web Programming in the LargeCompanion Proceedings of the The Web Conference 201810.1145/3184558.3185953(681-689)Online publication date: 23-Apr-2018
  • (2017)Formal methods for web securityJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2016.08.00687(110-126)Online publication date: Feb-2017
  • (2016)EliomProceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages10.1145/3064899.3064901(1-12)Online publication date: 31-Aug-2016
  • (2016)Process-aware web programming with JolieScience of Computer Programming10.1016/j.scico.2016.05.002130:C(69-96)Online publication date: 15-Nov-2016
  • (2015)Multitier Debugging of Web ApplicationsWeb Information Systems and Technologies10.1007/978-3-319-27030-2_3(33-47)Online publication date: 16-Dec-2015

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media