http://www.dagstuhl.de/14271

June 29 – July 4 , 2014, Dagstuhl Seminar 14271

Scripting Languages and Frameworks: Analysis and Verification

Organizers

Fritz Henglein (University of Copenhagen, DK)
Ranjit Jhala (University of California – San Diego, US)
Shriram Krishnamurthi (Brown University – Providence, US)
Peter Thiemann (Universität Freiburg, DE)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 4, Issue 6 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents

Summary

In the past decade scripting languages have become more mature: the wild experimentation and almost wilful embrace of obfuscation by Perl has been replaced by the level-headed simplicity of Python and the embrace of programming language research roots by Ruby. As a result, these languages have moved into the mainstream: every Web user relies on JavaScript.

The Challenges of Scripting Languages Though scripting languages have become more mature, from the perspective of building robust, reliable software, they still suffer from several distinct problems, each of which creates new challenges for the research community.

  • While these languages have textual definitions, they lack more formal descriptions, and in practice the textual "definitions" are themselves often in conflict with the normative nature of the implementations. This is in contrast to languages like Standard ML where the formal definition comes first. How far can we go in creating formal semantics from a combination of implementations and textual documents?
  • Tests -- more than either implementations, textual definitions, or formal semantics -- are becoming the norm for specification. For instance, the latest JavaScript standard explicitly embraces testing by publishing and regularly updating a conformance suite. Similarly, a team trying to create an alternate implementation of one of these languages may read the definition but what they really aspire to match is the test suite behavior. How can we support test suites as a new avenue of programming language specification?
  • One of the reasons programmers find these languages enjoyable (initially) is that they offer a variety of ``convenient'' features, such as overloading. As programs grow, however, understanding the full -- and unintended! -- behaviors of programs becomes a non-trivial effort. How can we design semantics and static and dynamic tools that can cope with the heavily understated and overloaded behaviors that make scripting languages attractive?
  • Programmers increasingly do not program in languages but in high-level frameworks built atop them. For instance, though "Ruby" is popular for Web programming, programmers rarely write Web applications directly in Ruby, but rather atop the higher-level Ruby on Rails platform. The result of imposing significantly higher-level interfaces is that they necessitate new reasoning modes. For instance, while the jQuery library is a pure JavaScript program, type-checking jQuery as if it were "merely" JavaScript would produce types that are both unreadably compex and relatively useless. Can we build custom reasoning at the level of the frameworks, then we can provide views of these frameworks that are consistent with the level at which developers think of them, and can we check that the implementations adhere to these interfaces?
  • These languages and frameworks are themselves not enough. They all reside in an eco-system of a family of other languages and frameworks whose interdependencies are necessary for proper understanding of program execution. For instance, in the client-side Web, JavaScript -- which has gotten significant attention from the research community -- only runs in response to stimuli, which are obtained from the DOM. In turn, the DOM and JavaScript both depend on the style-sheets written in CSS. But in fact all three of these components -- the JavaScript code, the CSS styling, and the DOM events -- all depend on one another, because almost any one can trigger or modify the other. Can we construct suitable abstractions such that each language can meaningfully talk about the others without importing an overwhelming amount of detail?

This seminar brought together a wide variety of researchers working on the above questions. The seminar was organized into a series of short and long talks on topics related to the above overarching questions, and four breakout sessions focussing on broader questions and challenges. Next, we briefly summarize the talks and sessions. The contributed talks focussed on the following over arching themes -- semantics, type systems, program analysis, contracts, languages and security.

License
  Creative Commons BY 3.0 Unported license
  Fritz Henglein, Ranjit Jhala, Shriram Krishnamurthi, and Peter Thiemann

Related Dagstuhl Seminar

Classification

  • Programming Languages / Compiler
  • Semantics / Formal Methods
  • Verification / Logic

Keywords

  • Semantics
  • Type systems
  • Verification techniques
  • Security analyses
  • Scalability
  • Rapid prototyping

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

NSF young researcher support