Dagstuhl Seminar 14271
Scripting Languages and Frameworks: Analysis and Verification
( Jun 29 – Jul 04, 2014 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/14271
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)
Contact
- Andreas Dolzmann (for scientific matters)
- Susanne Bach-Bernhard (for administrative matters)
Scripting languages have rapidly evolved over a few generations. Early languages like awk identified a need for unceremonious information extraction and manipulation, and showed that lightweight “dictionary" data structures were invaluable towards this end. Since the mid-1990s we have seen numerous such languages mushroom. Perhaps due to the increased sophistication of the prototyped systems, and the challenges of maintaining them, these languages have begun to mature and embrace language research roots.
Despite (and sometimes, because of) their maturity, several attributes of scripting languages make the task of using them to write robust and reliable software quite challenging.
Semantics: Most scripting languages lack formal descriptions, and those that exist are often at odds with actual implementations. In fact, more than reference implementations, tests are becoming the norm as a specification mechanism. Furthermore, features that make these languages seem convenient, like overloading, become a nuisance and complicate program comprehension. Thus, a key challenge is to support test suites as a new means of language specification, and to use them to design semantics and analyses that can cope with the ad-hoc special cases that make scripting languages attractive.
Strings: Due to their simplicity and universality, strings and dictionaries indexed by strings are the central datatypes in scripting languages, which makes it trivial for a script to communicate, with databases, devices, and over the network. Thus, to analyze the properties of a script, we must understand the idiomatic uses of strings in scripts and to develop theories to reason about them.
Frameworks: Programmers do not program so much in languages but in high-level frameworks like Rails, Django, Node, Backbone, and JQuery. Thus, a key challenge and opportunity is to develop simple framework-level reasoning systems (semantics, types, etc.).
Polyphony: Finally, it is not enough to reason about languages and frameworks in isolation as the essence of scripts is the gluing together of different sub-systems. The final challenge is to develop suitable abstractions that allow each language to meaningfully talk about the others without being drowned in detail.
The seminar will offer opportunities to not only discuss recent work in these areas but to also codify these research challenges and map out strategies for tackling them. The format will mix formal presentation with several informal and ad hoc sessions, thus preserving the feel of a true workshop while still giving participants an opportunity to stay abreast of research progress in this fast-moving field.
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.
Creative Commons BY 3.0 Unported license
Fritz Henglein, Ranjit Jhala, Shriram Krishnamurthi, and Peter Thiemann
- Achim D. Brucker (SAP SE - Karlsruhe, DE) [dblp]
- Niels Bjoern Bugge Grathwohl (University of Copenhagen, DK) [dblp]
- Ravi Chugh (University of California - San Diego, US) [dblp]
- Arlen Cox (University of Colorado - Boulder, US) [dblp]
- Christos Dimoulas (Harvard University - Cambridge, US) [dblp]
- Julian Dolby (IBM TJ Watson Research Center - Yorktown Heights, US) [dblp]
- Matthias Felleisen (Northeastern University - Boston, US) [dblp]
- Daniele Filaretti (Imperial College London, GB) [dblp]
- Cormac Flanagan (University of California - Santa Cruz, US) [dblp]
- Jeffrey Foster (University of Maryland - College Park, US)
- Ronald Garcia (University of British Columbia - Vancouver, CA) [dblp]
- Philippa Gardner (Imperial College London, GB) [dblp]
- Michael Greenberg (Princeton University, US) [dblp]
- Arjun Guha (University of Massachusetts - Amherst, US) [dblp]
- Shu-Yu Guo (MOZILLA - Mountain View, US)
- Christian Hammer (Universität des Saarlandes, DE) [dblp]
- Fritz Henglein (University of Copenhagen, DK) [dblp]
- Roberto Ierusalimschy (PUC - Rio de Janeiro, BR) [dblp]
- Thomas Jensen (INRIA Rennes - Bretagne Atlantique, FR) [dblp]
- Ranjit Jhala (University of California - San Diego, US) [dblp]
- Matthias Keil (Universität Freiburg, DE) [dblp]
- Shriram Krishnamurthi (Brown University - Providence, US) [dblp]
- Benjamin Lerner (Brown University - Providence, US) [dblp]
- Ben Livshits (Microsoft Corporation - Redmond, US) [dblp]
- Sergio Maffeis (Imperial College London, GB) [dblp]
- Matthew Might (University of Utah - Salt Lake City, US) [dblp]
- Yasuhiko Minamide (University of Tsukuba, JP) [dblp]
- Anders Møller (Aarhus University, DK) [dblp]
- Joseph Gibbs Politz (Brown University - Providence, US) [dblp]
- Ulrik Terp Rasmussen (University of Copenhagen, DK) [dblp]
- Tamara Rezk (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
- Tiark Rompf (EPFL - Lausanne, CH) [dblp]
- Sukyoung Ryu (KAIST - Daejeon, KR) [dblp]
- Alan Schmitt (INRIA Rennes - Bretagne Atlantique, FR) [dblp]
- Jeremy G. Siek (University of Colorado - Boulder, US) [dblp]
- Gareth Smith (Imperial College London, GB) [dblp]
- Manu Sridharan (Samsung Research - San Jose, US) [dblp]
- Éric Tanter (University of Chile - Santiago de Chile, CL) [dblp]
- Peter Thiemann (Universität Freiburg, DE) [dblp]
- Sam Tobin-Hochstadt (Indiana University - Bloomington, US) [dblp]
- Tom Van Cutsem (Alcatel-Lucent Bell Labs - Antwerp, BE) [dblp]
- David Van Horn (University of Maryland - College Park, US) [dblp]
- Panagiotis Vekris (University of California - San Diego, US) [dblp]
- Ben Wiedermann (Harvey Mudd College - Claremont, US) [dblp]
- Kwangkeun Yi (Seoul National University, KR) [dblp]
Related Seminars
- Dagstuhl Seminar 12011: Foundations for Scripting Languages (2012-01-02 - 2012-01-06) (Details)
Classification
- programming languages / compiler
- semantics / formal methods
- verification / logic
Keywords
- Semantics
- type systems
- verification techniques
- security analyses
- scalability
- rapid prototyping
