Onward! 2015 – Author Index |
Contents -
Abstracts -
Authors
|
A B C D E F G H I J K L M N O P R S T W
| Afroozeh, Ali |
Onward! '15: "One Parser to Rule Them All ..."
One Parser to Rule Them All
Ali Afroozeh and Anastasia Izmaylova (CWI, Netherlands) Despite the long history of research in parsing, constructing parsers for real programming languages remains a difficult and painful task. In the last decades, different parser generators emerged to allow the construction of parsers from a BNF-like specification. However, still today, many parsers are handwritten, or are only partly generated, and include various hacks to deal with different peculiarities in programming languages. The main problem is that current declarative syntax definition techniques are based on pure context-free grammars, while many constructs found in programming languages require context information. In this paper we propose a parsing framework that embraces context information in its core. Our framework is based on data-dependent grammars, which extend context-free grammars with arbitrary computation, variable binding and constraints. We present an implementation of our framework on top of the Generalized LL (GLL) parsing algorithm, and show how common idioms in syntax of programming languages such as (1) lexical disambiguation filters, (2) operator precedence, (3) indentation-sensitive rules, and (4) conditional preprocessor directives can be mapped to data-dependent grammars. We demonstrate the initial experience with our framework, by parsing more than 20000 Java, C#, Haskell, and OCaml source files. 
@InProceedings{Onward!15p151,
author = {Ali Afroozeh and Anastasia Izmaylova},
title = {One Parser to Rule Them All},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {151--170},
doi = {},
year = {2015},
}
 Info
|
|
| Ali, Karim |
Onward! '15: "Towards Secure Integration ..."
Towards Secure Integration of Cryptographic Software
Steven Arzt, Sarah Nadi, Karim Ali, Eric Bodden, Sebastian Erdweg, and Mira Mezini (TU Darmstadt, Germany) While cryptography is now readily available to everyone and can, provably, protect private information from attackers, we still frequently hear about major data leakages, many of which are due to improper use of cryptographic mechanisms. The problem is that many application developers are not cryptographic experts. Even though high-quality cryptographic APIs are widely available, programmers often select the wrong algorithms or misuse APIs due to a lack of understanding. Such issues arise with both simple operations such as encryption as well as with complex secure communication protocols such as SSL. In this paper, we provide a long-term solution that helps application developers integrate cryptographic components correctly and securely by bridging the gap between cryptographers and application developers. Our solution consists of a software product line (with an underlying feature model) that automatically identifies the correct cryptographic algorithms to use, based on the developer's answers to high-level questions in non-expert terminology. Each feature (i.e., cryptographic algorithm) maps into corresponding Java code and a usage protocol describing API restrictions. By composing the user's selected features, we automatically synthesize a secure code blueprint and a usage protocol that corresponds to the selected usage scenario. Since the developer may change the application code over time, we use the usage protocols to statically analyze the program and ensure that the correct use of the API is not violated over time.
@InProceedings{Onward!15p1,
author = {Steven Arzt and Sarah Nadi and Karim Ali and Eric Bodden and Sebastian Erdweg and Mira Mezini},
title = {Towards Secure Integration of Cryptographic Software},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {1--13},
doi = {},
year = {2015},
}
|
|
| Appeltauer, Malte |
Onward! '15: "Columnar Objects: Improving ..."
Columnar Objects: Improving the Performance of Analytical Applications
Toni Mattis, Johannes Henning, Patrick Rein, Robert Hirschfeld, and Malte Appeltauer (HPI, Germany; SAP, Germany) Growing volumes of data increase the demand to use it in analytical applications to make informed decisions. Unfortunately, object-oriented runtimes experience performance problems when dealing with large data volumes. Similar problems have been addressed by column-oriented in-memory databases, whose memory layout is tailored to analytical workloads. As a result, data storage and processing are often delegated to such a database. However, the more domain logic is moved to this separate system, the more benefits of object-orientation are lost. We propose modifications to dynamic object-oriented runtimes to store collections of objects in a column-oriented memory layout and leverage a jit to take advantage of the adjusted layout by mapping object traversal to array operations. We implemented our concept in PyPy, a Python interpreter equipped with a tracing jit. Finally, we show that analytical algorithms, expressed through object-oriented code, are up to three times faster due to our optimizations, without substantially impairing the paradigm. Hopefully, extending these concepts will mitigate some problems originating from the paradigm mismatch between object-oriented runtimes and databases.
@InProceedings{Onward!15p197,
author = {Toni Mattis and Johannes Henning and Patrick Rein and Robert Hirschfeld and Malte Appeltauer},
title = {Columnar Objects: Improving the Performance of Analytical Applications},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {197--210},
doi = {},
year = {2015},
}
|
|
| Arzt, Steven |
Onward! '15: "Towards Secure Integration ..."
Towards Secure Integration of Cryptographic Software
Steven Arzt, Sarah Nadi, Karim Ali, Eric Bodden, Sebastian Erdweg, and Mira Mezini (TU Darmstadt, Germany) While cryptography is now readily available to everyone and can, provably, protect private information from attackers, we still frequently hear about major data leakages, many of which are due to improper use of cryptographic mechanisms. The problem is that many application developers are not cryptographic experts. Even though high-quality cryptographic APIs are widely available, programmers often select the wrong algorithms or misuse APIs due to a lack of understanding. Such issues arise with both simple operations such as encryption as well as with complex secure communication protocols such as SSL. In this paper, we provide a long-term solution that helps application developers integrate cryptographic components correctly and securely by bridging the gap between cryptographers and application developers. Our solution consists of a software product line (with an underlying feature model) that automatically identifies the correct cryptographic algorithms to use, based on the developer's answers to high-level questions in non-expert terminology. Each feature (i.e., cryptographic algorithm) maps into corresponding Java code and a usage protocol describing API restrictions. By composing the user's selected features, we automatically synthesize a secure code blueprint and a usage protocol that corresponds to the selected usage scenario. Since the developer may change the application code over time, we use the usage protocols to statically analyze the program and ensure that the correct use of the API is not violated over time.
@InProceedings{Onward!15p1,
author = {Steven Arzt and Sarah Nadi and Karim Ali and Eric Bodden and Sebastian Erdweg and Mira Mezini},
title = {Towards Secure Integration of Cryptographic Software},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {1--13},
doi = {},
year = {2015},
}
|
|
| Barman, Shaon |
Onward! '15: "Toward Tool Support for Interactive ..."
Toward Tool Support for Interactive Synthesis
Shaon Barman, Rastislav Bodik, Satish Chandra, Emina Torlak, Arka Bhattacharya, and David Culler (University of California at Berkeley, USA; University of Washington, USA; Samsung Research, USA) Syntax-guided synthesis searches for an implementation of a given specification by exploring large spaces of candidate programs. Sketches reduce these search spaces, making synthesis more tractable, by predefining the structure of the desired implementation. Typically, this structure is obtained through human insight---this paper introduces a method for interactive, tool-supported discovery of such structure. The key idea is to decompose the specification into subcomputations such that the decomposition dictates the sketch. We rely on a readily obtainable specification that is nothing more than a finite set of sample input-output pairs or execution traces of the desired program. We introduce two complementary decomposition operators and demonstrate them on case studies. We find that our interactive methodology to discover structure extends the reach of computer-aided programming to problems that cannot be solved with synthesis alone.
@InProceedings{Onward!15p121,
author = {Shaon Barman and Rastislav Bodik and Satish Chandra and Emina Torlak and Arka Bhattacharya and David Culler},
title = {Toward Tool Support for Interactive Synthesis},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {121--136},
doi = {},
year = {2015},
}
|
|
| Bhattacharya, Arka |
Onward! '15: "Toward Tool Support for Interactive ..."
Toward Tool Support for Interactive Synthesis
Shaon Barman, Rastislav Bodik, Satish Chandra, Emina Torlak, Arka Bhattacharya, and David Culler (University of California at Berkeley, USA; University of Washington, USA; Samsung Research, USA) Syntax-guided synthesis searches for an implementation of a given specification by exploring large spaces of candidate programs. Sketches reduce these search spaces, making synthesis more tractable, by predefining the structure of the desired implementation. Typically, this structure is obtained through human insight---this paper introduces a method for interactive, tool-supported discovery of such structure. The key idea is to decompose the specification into subcomputations such that the decomposition dictates the sketch. We rely on a readily obtainable specification that is nothing more than a finite set of sample input-output pairs or execution traces of the desired program. We introduce two complementary decomposition operators and demonstrate them on case studies. We find that our interactive methodology to discover structure extends the reach of computer-aided programming to problems that cannot be solved with synthesis alone.
@InProceedings{Onward!15p121,
author = {Shaon Barman and Rastislav Bodik and Satish Chandra and Emina Torlak and Arka Bhattacharya and David Culler},
title = {Toward Tool Support for Interactive Synthesis},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {121--136},
doi = {},
year = {2015},
}
|
|
| Bodden, Eric |
Onward! '15: "Towards Secure Integration ..."
Towards Secure Integration of Cryptographic Software
Steven Arzt, Sarah Nadi, Karim Ali, Eric Bodden, Sebastian Erdweg, and Mira Mezini (TU Darmstadt, Germany) While cryptography is now readily available to everyone and can, provably, protect private information from attackers, we still frequently hear about major data leakages, many of which are due to improper use of cryptographic mechanisms. The problem is that many application developers are not cryptographic experts. Even though high-quality cryptographic APIs are widely available, programmers often select the wrong algorithms or misuse APIs due to a lack of understanding. Such issues arise with both simple operations such as encryption as well as with complex secure communication protocols such as SSL. In this paper, we provide a long-term solution that helps application developers integrate cryptographic components correctly and securely by bridging the gap between cryptographers and application developers. Our solution consists of a software product line (with an underlying feature model) that automatically identifies the correct cryptographic algorithms to use, based on the developer's answers to high-level questions in non-expert terminology. Each feature (i.e., cryptographic algorithm) maps into corresponding Java code and a usage protocol describing API restrictions. By composing the user's selected features, we automatically synthesize a secure code blueprint and a usage protocol that corresponds to the selected usage scenario. Since the developer may change the application code over time, we use the usage protocols to statically analyze the program and ensure that the correct use of the API is not violated over time.
@InProceedings{Onward!15p1,
author = {Steven Arzt and Sarah Nadi and Karim Ali and Eric Bodden and Sebastian Erdweg and Mira Mezini},
title = {Towards Secure Integration of Cryptographic Software},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {1--13},
doi = {},
year = {2015},
}
|
|
| Bodik, Rastislav |
Onward! '15: "Toward Tool Support for Interactive ..."
Toward Tool Support for Interactive Synthesis
Shaon Barman, Rastislav Bodik, Satish Chandra, Emina Torlak, Arka Bhattacharya, and David Culler (University of California at Berkeley, USA; University of Washington, USA; Samsung Research, USA) Syntax-guided synthesis searches for an implementation of a given specification by exploring large spaces of candidate programs. Sketches reduce these search spaces, making synthesis more tractable, by predefining the structure of the desired implementation. Typically, this structure is obtained through human insight---this paper introduces a method for interactive, tool-supported discovery of such structure. The key idea is to decompose the specification into subcomputations such that the decomposition dictates the sketch. We rely on a readily obtainable specification that is nothing more than a finite set of sample input-output pairs or execution traces of the desired program. We introduce two complementary decomposition operators and demonstrate them on case studies. We find that our interactive methodology to discover structure extends the reach of computer-aided programming to problems that cannot be solved with synthesis alone.
@InProceedings{Onward!15p121,
author = {Shaon Barman and Rastislav Bodik and Satish Chandra and Emina Torlak and Arka Bhattacharya and David Culler},
title = {Toward Tool Support for Interactive Synthesis},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {121--136},
doi = {},
year = {2015},
}
|
|
| Borning, Alan |
Onward! '15: "Constraints as a Design Pattern ..."
Constraints as a Design Pattern
Hesam Samimi, Alessandro Warth, Mahdi Eslamimehr, and Alan Borning (SAP Labs, USA; Viewpoints Research Institute, USA) Imperative programming has great merits. As the ubiquitous style, it is familiar, and its linear and step by step nature is favored by the human mind. Experienced programmers, however, are aware of its major flaw: it is easy for meanings to get lost in piles of code, making software hard to understand, extend, and debug. Constraint-based programming as an alternative has been observed to suffer much less from these flaws, where the "what" (the intention) is expressed rather than the "how" (the algorithm) in performing a computation. It is the job of the system to automatically achieve the intention through constraint solving. Sadly, poor performance and expressiveness has prevented this style from seeing widespread adoption. We propose a general programming model as a kind of a sweet spot between imperative and constraint-based programming. Our aim is to leverage many benefits of constraint-based programming such as understandability, behavioral modularity, extensibility, etc., in a practical way and without suffering the breakdown of the approach as with the traditional constraint-based paradigm. This model enforces a certain organization where at the top-level a program is simply composed of a set of constraints. However, the constraints aren't necessarily solved by an external entity, and the programmer uses imperative code to specify (1) how each constraint should be solved in isolation, and (2) how to combine individual solutions. We have implemented a tool called Sketchpad14 that incorporates this model in JavaScript, and built a number of realistic applications in it. In this paper we demonstrate the merits of our approach by comparing it with traditional imperative as well as constraint-based approaches.
@InProceedings{Onward!15p28,
author = {Hesam Samimi and Alessandro Warth and Mahdi Eslamimehr and Alan Borning},
title = {Constraints as a Design Pattern},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {28--43},
doi = {},
year = {2015},
}
Info
|
|
| Bouraqadi, Noury |
Onward! '15: "A Bootstrapping Infrastructure ..."
A Bootstrapping Infrastructure to Build and Extend Pharo-Like Languages
Guillermo Polito, Stéphane Ducasse, Noury Bouraqadi, and Luc Fabresse (INRIA, France; École des Mines de Douai, France) Bootstrapping is well known in the context of compilers, where a bootstrapped compiler can compile its own source code. Bootstrapping is a beneficial engineering practice because it raises the level of abstraction of a program making it easier to understand, optimize, evolve, etc. Bootstrapping a reflective object-oriented language is however more challenging, as we need also to initialize the runtime of the language with its initial objects and classes besides writing its compiler. In this paper, we present a novel bootstrapping infrastructure for Pharo-like languages that allows us to easily extend and modify such languages. Our bootstrapping process relies on a first-class runtime. A first-class runtime is a meta-object that represents a program’s runtime and provides a MOP to easily load code into it and manipulate its objects. It decouples the virtual machine (VM) and language concerns by introducing a clear VM-language interface. Using this process, we show how we succeeded to bootstrap a Smalltalk-based language named Candle and then extend it with traits in less than 250 lines of high-level Smalltalk code. We also show how we can bootstrap with minimal effort two other languages (Pharo and MetaTalk) with similar execution semantics but different object models.
@InProceedings{Onward!15p183,
author = {Guillermo Polito and Stéphane Ducasse and Noury Bouraqadi and Luc Fabresse},
title = {A Bootstrapping Infrastructure to Build and Extend Pharo-Like Languages},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {183--196},
doi = {},
year = {2015},
}
Onward! '15: "Virtualization Support for ..."
Virtualization Support for Dynamic Core Library Update
Guillermo Polito, Stéphane Ducasse, Noury Bouraqadi, Luc Fabresse, and Max Mattone (INRIA, France; École des Mines de Douai, France) Dynamically updating language runtime and core libraries such as collections and threading is challenging since the update mechanism uses such libraries at the same time that it modifies them. To tackle this challenge, we present Dy- namic Core Library Update (DCU) as an extension of Dy- namic Software Update (DSU) and our approach based on a virtualization architecture. Our solution supports the up- date of core libraries as any other normal library, avoiding the circular dependencies between the updater and the core libraries. Our benchmarks show that there is no evident per- formance overhead in comparison with a default execution. Finally, we show that our approach can be applied to real life scenario by introducing a critical update inside a web application with 20 simulated concurrent users.
@InProceedings{Onward!15p211,
author = {Guillermo Polito and Stéphane Ducasse and Noury Bouraqadi and Luc Fabresse and Max Mattone},
title = {Virtualization Support for Dynamic Core Library Update},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {211--223},
doi = {},
year = {2015},
}
|
|
| Chandra, Satish |
Onward! '15: "Toward Tool Support for Interactive ..."
Toward Tool Support for Interactive Synthesis
Shaon Barman, Rastislav Bodik, Satish Chandra, Emina Torlak, Arka Bhattacharya, and David Culler (University of California at Berkeley, USA; University of Washington, USA; Samsung Research, USA) Syntax-guided synthesis searches for an implementation of a given specification by exploring large spaces of candidate programs. Sketches reduce these search spaces, making synthesis more tractable, by predefining the structure of the desired implementation. Typically, this structure is obtained through human insight---this paper introduces a method for interactive, tool-supported discovery of such structure. The key idea is to decompose the specification into subcomputations such that the decomposition dictates the sketch. We rely on a readily obtainable specification that is nothing more than a finite set of sample input-output pairs or execution traces of the desired program. We introduce two complementary decomposition operators and demonstrate them on case studies. We find that our interactive methodology to discover structure extends the reach of computer-aided programming to problems that cannot be solved with synthesis alone.
@InProceedings{Onward!15p121,
author = {Shaon Barman and Rastislav Bodik and Satish Chandra and Emina Torlak and Arka Bhattacharya and David Culler},
title = {Toward Tool Support for Interactive Synthesis},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {121--136},
doi = {},
year = {2015},
}
|
|
| Chari, Guido |
Onward! '15: "Towards Fully Reflective Environments ..."
Towards Fully Reflective Environments
Guido Chari, Diego Garbervetsky, Stefan Marr, and Stéphane Ducasse (CONICET, Argentina; University of Buenos Aires, Argentina; INRIA, France) Modern development environments promote live programming (LP) mechanisms because it enhances the development experience by providing instantaneous feedback and interaction with live objects. LP is typically supported with advanced reflective techniques within dynamic languages. These languages run on top of Virtual Machines (VMs) that are built in a static manner so that most of their components are bound at compile time. As a consequence, VM developers are forced to work using the traditional edit-compile-run cycle, even when they are designing LP-supporting environments. In this paper we explore the idea of bringing LP techniques to the VM domain for improving their observability, evolution and adaptability at run-time. We define the notion of fully reflective execution environments (EEs), systems that provide reflection not only at the application level but also at the level of the VM. We characterize such systems, propose a design, and present Mate v1, a prototypical implementation. Based on our prototype, we analyze the feasibility and applicability of incorporating reflective capabilities into different parts of EEs. Furthermore, the evaluation demonstrates the opportunities such reflective capabilities provide for unanticipated dynamic adaptation scenarios, benefiting thus, a wider range of users.
@InProceedings{Onward!15p240,
author = {Guido Chari and Diego Garbervetsky and Stefan Marr and Stéphane Ducasse},
title = {Towards Fully Reflective Environments},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {240--253},
doi = {},
year = {2015},
}
|
|
| Chiş, Andrei |
Onward! '15: "The Moldable Inspector ..."
The Moldable Inspector
Andrei Chiş, Oscar Nierstrasz, Aliaksei Syrel, and Tudor Gîrba (University of Bern, Switzerland; tudorgirba.com, Switzerland) Object inspectors are an essential category of tools that allow developers to comprehend the run-time of object-oriented systems. Traditional object inspectors favor a generic view that focuses on the low-level details of the state of single objects. Based on 16 interviews with software developers and a follow-up survey with 62 respondents we identified a need for object inspectors that support different high-level ways to visualize and explore objects, depending on both the object and the current developer need. We propose the Moldable Inspector, a novel inspector model that enables developers to adapt the inspection workflow to suit their immediate needs by making the inspection context explicit, providing multiple interchangeable domain-specific views for each object, and supporting a workflow that groups together multiple levels of connected objects. We show that the Moldable Inspector can address multiple kinds of development needs involving a wide range of objects.
@InProceedings{Onward!15p44,
author = {Andrei Chiş and Oscar Nierstrasz and Aliaksei Syrel and Tudor Gîrba},
title = {The Moldable Inspector},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {44--60},
doi = {},
year = {2015},
}
Info
|
|
| Cito, Jürgen |
Onward! '15: "Runtime Metric Meets Developer: ..."
Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback
Jürgen Cito, Philipp Leitner, Harald C. Gall, Aryan Dadashi, Anne Keller, and Andreas Roth (University of Zurich, Switzerland; SAP, Germany) A unifying theme of many ongoing trends in software engineering is a blurring of the boundaries between building and operating software products. In this paper, we explore what we consider to be the logical next step in this succession: integrating runtime monitoring data from production deployments of the software into the tools developers utilize in their daily workflows (i.e., IDEs) to enable tighter feedback loops. We refer to this notion as feedback-driven development (FDD). This more abstract FDD concept can be instantiated in various ways, ranging from IDE plugins that implement feedback-driven refactoring and code optimization to plugins that predict performance and cost implications of code changes prior to even deploying the new version of the soft- ware. We demonstrate existing proof-of-concept realizations of these ideas and illustrate our vision of the future of FDD and cloud-based software development in general. Further, we discuss the major challenges that need to be solved be- fore FDD can achieve mainstream adoption.
@InProceedings{Onward!15p14,
author = {Jürgen Cito and Philipp Leitner and Harald C. Gall and Aryan Dadashi and Anne Keller and Andreas Roth},
title = {Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {14--27},
doi = {},
year = {2015},
}
|
|
| Culler, David |
Onward! '15: "Toward Tool Support for Interactive ..."
Toward Tool Support for Interactive Synthesis
Shaon Barman, Rastislav Bodik, Satish Chandra, Emina Torlak, Arka Bhattacharya, and David Culler (University of California at Berkeley, USA; University of Washington, USA; Samsung Research, USA) Syntax-guided synthesis searches for an implementation of a given specification by exploring large spaces of candidate programs. Sketches reduce these search spaces, making synthesis more tractable, by predefining the structure of the desired implementation. Typically, this structure is obtained through human insight---this paper introduces a method for interactive, tool-supported discovery of such structure. The key idea is to decompose the specification into subcomputations such that the decomposition dictates the sketch. We rely on a readily obtainable specification that is nothing more than a finite set of sample input-output pairs or execution traces of the desired program. We introduce two complementary decomposition operators and demonstrate them on case studies. We find that our interactive methodology to discover structure extends the reach of computer-aided programming to problems that cannot be solved with synthesis alone.
@InProceedings{Onward!15p121,
author = {Shaon Barman and Rastislav Bodik and Satish Chandra and Emina Torlak and Arka Bhattacharya and David Culler},
title = {Toward Tool Support for Interactive Synthesis},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {121--136},
doi = {},
year = {2015},
}
|
|
| Dadashi, Aryan |
Onward! '15: "Runtime Metric Meets Developer: ..."
Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback
Jürgen Cito, Philipp Leitner, Harald C. Gall, Aryan Dadashi, Anne Keller, and Andreas Roth (University of Zurich, Switzerland; SAP, Germany) A unifying theme of many ongoing trends in software engineering is a blurring of the boundaries between building and operating software products. In this paper, we explore what we consider to be the logical next step in this succession: integrating runtime monitoring data from production deployments of the software into the tools developers utilize in their daily workflows (i.e., IDEs) to enable tighter feedback loops. We refer to this notion as feedback-driven development (FDD). This more abstract FDD concept can be instantiated in various ways, ranging from IDE plugins that implement feedback-driven refactoring and code optimization to plugins that predict performance and cost implications of code changes prior to even deploying the new version of the soft- ware. We demonstrate existing proof-of-concept realizations of these ideas and illustrate our vision of the future of FDD and cloud-based software development in general. Further, we discuss the major challenges that need to be solved be- fore FDD can achieve mainstream adoption.
@InProceedings{Onward!15p14,
author = {Jürgen Cito and Philipp Leitner and Harald C. Gall and Aryan Dadashi and Anne Keller and Andreas Roth},
title = {Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {14--27},
doi = {},
year = {2015},
}
|
|
| De Koster, Joeri |
Onward! '15: "Just-in-Time Data Structures ..."
Just-in-Time Data Structures
Mattias De Wael, Stefan Marr, Joeri De Koster, Jennifer B. Sartor, and Wolfgang De Meuter (Vrije Universiteit Brussel, Belgium; INRIA, France; Ghent University, Belgium) Today, software engineering practices focus on finding the single ``right'' data representation for a program. The ``right'' data representation, however, might not exist: changing the representation of an object during program execution can be better in terms of performance. To this end we introduce Just-in-Time Data Structures, which enable representation changes at runtime, based on declarative input from a performance expert programmer. Just-in-Time Data Structures are an attempt to shift the focus from finding the ``right'' data structure to finding the ``right'' sequence of data representations. We present JitDS, a programming language to develop such Just-in-Time Data Structures. Further, we show two example programs that benefit from changing the representation at runtime.
@InProceedings{Onward!15p61,
author = {Mattias De Wael and Stefan Marr and Joeri De Koster and Jennifer B. Sartor and Wolfgang De Meuter},
title = {Just-in-Time Data Structures},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {61--75},
doi = {},
year = {2015},
}
Info
|
|
| De Meuter, Wolfgang |
Onward! '15: "Just-in-Time Data Structures ..."
Just-in-Time Data Structures
Mattias De Wael, Stefan Marr, Joeri De Koster, Jennifer B. Sartor, and Wolfgang De Meuter (Vrije Universiteit Brussel, Belgium; INRIA, France; Ghent University, Belgium) Today, software engineering practices focus on finding the single ``right'' data representation for a program. The ``right'' data representation, however, might not exist: changing the representation of an object during program execution can be better in terms of performance. To this end we introduce Just-in-Time Data Structures, which enable representation changes at runtime, based on declarative input from a performance expert programmer. Just-in-Time Data Structures are an attempt to shift the focus from finding the ``right'' data structure to finding the ``right'' sequence of data representations. We present JitDS, a programming language to develop such Just-in-Time Data Structures. Further, we show two example programs that benefit from changing the representation at runtime.
@InProceedings{Onward!15p61,
author = {Mattias De Wael and Stefan Marr and Joeri De Koster and Jennifer B. Sartor and Wolfgang De Meuter},
title = {Just-in-Time Data Structures},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {61--75},
doi = {},
year = {2015},
}
Info
|
|
| De Wael, Mattias |
Onward! '15: "Just-in-Time Data Structures ..."
Just-in-Time Data Structures
Mattias De Wael, Stefan Marr, Joeri De Koster, Jennifer B. Sartor, and Wolfgang De Meuter (Vrije Universiteit Brussel, Belgium; INRIA, France; Ghent University, Belgium) Today, software engineering practices focus on finding the single ``right'' data representation for a program. The ``right'' data representation, however, might not exist: changing the representation of an object during program execution can be better in terms of performance. To this end we introduce Just-in-Time Data Structures, which enable representation changes at runtime, based on declarative input from a performance expert programmer. Just-in-Time Data Structures are an attempt to shift the focus from finding the ``right'' data structure to finding the ``right'' sequence of data representations. We present JitDS, a programming language to develop such Just-in-Time Data Structures. Further, we show two example programs that benefit from changing the representation at runtime.
@InProceedings{Onward!15p61,
author = {Mattias De Wael and Stefan Marr and Joeri De Koster and Jennifer B. Sartor and Wolfgang De Meuter},
title = {Just-in-Time Data Structures},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {61--75},
doi = {},
year = {2015},
}
Info
|
|
 |
Ducasse, Stéphane |
Onward! '15: "A Bootstrapping Infrastructure ..."
A Bootstrapping Infrastructure to Build and Extend Pharo-Like Languages
Guillermo Polito, Stéphane Ducasse, Noury Bouraqadi, and Luc Fabresse (INRIA, France; École des Mines de Douai, France) Bootstrapping is well known in the context of compilers, where a bootstrapped compiler can compile its own source code. Bootstrapping is a beneficial engineering practice because it raises the level of abstraction of a program making it easier to understand, optimize, evolve, etc. Bootstrapping a reflective object-oriented language is however more challenging, as we need also to initialize the runtime of the language with its initial objects and classes besides writing its compiler. In this paper, we present a novel bootstrapping infrastructure for Pharo-like languages that allows us to easily extend and modify such languages. Our bootstrapping process relies on a first-class runtime. A first-class runtime is a meta-object that represents a program’s runtime and provides a MOP to easily load code into it and manipulate its objects. It decouples the virtual machine (VM) and language concerns by introducing a clear VM-language interface. Using this process, we show how we succeeded to bootstrap a Smalltalk-based language named Candle and then extend it with traits in less than 250 lines of high-level Smalltalk code. We also show how we can bootstrap with minimal effort two other languages (Pharo and MetaTalk) with similar execution semantics but different object models.
@InProceedings{Onward!15p183,
author = {Guillermo Polito and Stéphane Ducasse and Noury Bouraqadi and Luc Fabresse},
title = {A Bootstrapping Infrastructure to Build and Extend Pharo-Like Languages},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {183--196},
doi = {},
year = {2015},
}
Onward! '15: "Towards Fully Reflective Environments ..."
Towards Fully Reflective Environments
Guido Chari, Diego Garbervetsky, Stefan Marr, and Stéphane Ducasse (CONICET, Argentina; University of Buenos Aires, Argentina; INRIA, France) Modern development environments promote live programming (LP) mechanisms because it enhances the development experience by providing instantaneous feedback and interaction with live objects. LP is typically supported with advanced reflective techniques within dynamic languages. These languages run on top of Virtual Machines (VMs) that are built in a static manner so that most of their components are bound at compile time. As a consequence, VM developers are forced to work using the traditional edit-compile-run cycle, even when they are designing LP-supporting environments. In this paper we explore the idea of bringing LP techniques to the VM domain for improving their observability, evolution and adaptability at run-time. We define the notion of fully reflective execution environments (EEs), systems that provide reflection not only at the application level but also at the level of the VM. We characterize such systems, propose a design, and present Mate v1, a prototypical implementation. Based on our prototype, we analyze the feasibility and applicability of incorporating reflective capabilities into different parts of EEs. Furthermore, the evaluation demonstrates the opportunities such reflective capabilities provide for unanticipated dynamic adaptation scenarios, benefiting thus, a wider range of users.
@InProceedings{Onward!15p240,
author = {Guido Chari and Diego Garbervetsky and Stefan Marr and Stéphane Ducasse},
title = {Towards Fully Reflective Environments},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {240--253},
doi = {},
year = {2015},
}
Onward! '15: "Virtualization Support for ..."
Virtualization Support for Dynamic Core Library Update
Guillermo Polito, Stéphane Ducasse, Noury Bouraqadi, Luc Fabresse, and Max Mattone (INRIA, France; École des Mines de Douai, France) Dynamically updating language runtime and core libraries such as collections and threading is challenging since the update mechanism uses such libraries at the same time that it modifies them. To tackle this challenge, we present Dy- namic Core Library Update (DCU) as an extension of Dy- namic Software Update (DSU) and our approach based on a virtualization architecture. Our solution supports the up- date of core libraries as any other normal library, avoiding the circular dependencies between the updater and the core libraries. Our benchmarks show that there is no evident per- formance overhead in comparison with a default execution. Finally, we show that our approach can be applied to real life scenario by introducing a critical update inside a web application with 20 simulated concurrent users.
@InProceedings{Onward!15p211,
author = {Guillermo Polito and Stéphane Ducasse and Noury Bouraqadi and Luc Fabresse and Max Mattone},
title = {Virtualization Support for Dynamic Core Library Update},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {211--223},
doi = {},
year = {2015},
}
|
| Erdweg, Sebastian |
Onward! '15: "Type Systems for the Masses: ..."
Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers
Sylvia Grewe, Sebastian Erdweg, Pascal Wittmann, and Mira Mezini (TU Darmstadt, Germany; Lancaster University, UK) The correct definition and implementation of non-trivial type systems is difficult and requires expert knowledge, which is not available to developers of domain-specific languages (DSLs) in practice. We propose Veritas, a workbench that simplifies the development of sound type systems. Veritas provides a single, high-level specification language for type systems, from which it automatically tries to derive soundness proofs and efficient and correct type-checking algorithms. For verification, Veritas combines off-the-shelf automated first-order theorem provers with automated proof strategies specific to type systems. For deriving efficient type checkers, Veritas provides a collection of optimization strategies whose applicability to a given type system is checked through verification on a case-by-case basis. We have developed a prototypical implementation of Veritas and used it to verify type soundness of the simply-typed lambda calculus and of parts of typed SQL. Our experience suggests that many of the individual verification steps can be automated and, in particular, that a high degree of automation is possible for type systems of DSLs.
@InProceedings{Onward!15p137,
author = {Sylvia Grewe and Sebastian Erdweg and Pascal Wittmann and Mira Mezini},
title = {Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {137--150},
doi = {},
year = {2015},
}
Onward! '15: "Towards Secure Integration ..."
Towards Secure Integration of Cryptographic Software
Steven Arzt, Sarah Nadi, Karim Ali, Eric Bodden, Sebastian Erdweg, and Mira Mezini (TU Darmstadt, Germany) While cryptography is now readily available to everyone and can, provably, protect private information from attackers, we still frequently hear about major data leakages, many of which are due to improper use of cryptographic mechanisms. The problem is that many application developers are not cryptographic experts. Even though high-quality cryptographic APIs are widely available, programmers often select the wrong algorithms or misuse APIs due to a lack of understanding. Such issues arise with both simple operations such as encryption as well as with complex secure communication protocols such as SSL. In this paper, we provide a long-term solution that helps application developers integrate cryptographic components correctly and securely by bridging the gap between cryptographers and application developers. Our solution consists of a software product line (with an underlying feature model) that automatically identifies the correct cryptographic algorithms to use, based on the developer's answers to high-level questions in non-expert terminology. Each feature (i.e., cryptographic algorithm) maps into corresponding Java code and a usage protocol describing API restrictions. By composing the user's selected features, we automatically synthesize a secure code blueprint and a usage protocol that corresponds to the selected usage scenario. Since the developer may change the application code over time, we use the usage protocols to statically analyze the program and ensure that the correct use of the API is not violated over time.
@InProceedings{Onward!15p1,
author = {Steven Arzt and Sarah Nadi and Karim Ali and Eric Bodden and Sebastian Erdweg and Mira Mezini},
title = {Towards Secure Integration of Cryptographic Software},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {1--13},
doi = {},
year = {2015},
}
|
|
| Eslamimehr, Mahdi |
Onward! '15: "Constraints as a Design Pattern ..."
Constraints as a Design Pattern
Hesam Samimi, Alessandro Warth, Mahdi Eslamimehr, and Alan Borning (SAP Labs, USA; Viewpoints Research Institute, USA) Imperative programming has great merits. As the ubiquitous style, it is familiar, and its linear and step by step nature is favored by the human mind. Experienced programmers, however, are aware of its major flaw: it is easy for meanings to get lost in piles of code, making software hard to understand, extend, and debug. Constraint-based programming as an alternative has been observed to suffer much less from these flaws, where the "what" (the intention) is expressed rather than the "how" (the algorithm) in performing a computation. It is the job of the system to automatically achieve the intention through constraint solving. Sadly, poor performance and expressiveness has prevented this style from seeing widespread adoption. We propose a general programming model as a kind of a sweet spot between imperative and constraint-based programming. Our aim is to leverage many benefits of constraint-based programming such as understandability, behavioral modularity, extensibility, etc., in a practical way and without suffering the breakdown of the approach as with the traditional constraint-based paradigm. This model enforces a certain organization where at the top-level a program is simply composed of a set of constraints. However, the constraints aren't necessarily solved by an external entity, and the programmer uses imperative code to specify (1) how each constraint should be solved in isolation, and (2) how to combine individual solutions. We have implemented a tool called Sketchpad14 that incorporates this model in JavaScript, and built a number of realistic applications in it. In this paper we demonstrate the merits of our approach by comparing it with traditional imperative as well as constraint-based approaches.
@InProceedings{Onward!15p28,
author = {Hesam Samimi and Alessandro Warth and Mahdi Eslamimehr and Alan Borning},
title = {Constraints as a Design Pattern},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {28--43},
doi = {},
year = {2015},
}
Info
|
|
| Fabresse, Luc |
Onward! '15: "A Bootstrapping Infrastructure ..."
A Bootstrapping Infrastructure to Build and Extend Pharo-Like Languages
Guillermo Polito, Stéphane Ducasse, Noury Bouraqadi, and Luc Fabresse (INRIA, France; École des Mines de Douai, France) Bootstrapping is well known in the context of compilers, where a bootstrapped compiler can compile its own source code. Bootstrapping is a beneficial engineering practice because it raises the level of abstraction of a program making it easier to understand, optimize, evolve, etc. Bootstrapping a reflective object-oriented language is however more challenging, as we need also to initialize the runtime of the language with its initial objects and classes besides writing its compiler. In this paper, we present a novel bootstrapping infrastructure for Pharo-like languages that allows us to easily extend and modify such languages. Our bootstrapping process relies on a first-class runtime. A first-class runtime is a meta-object that represents a program’s runtime and provides a MOP to easily load code into it and manipulate its objects. It decouples the virtual machine (VM) and language concerns by introducing a clear VM-language interface. Using this process, we show how we succeeded to bootstrap a Smalltalk-based language named Candle and then extend it with traits in less than 250 lines of high-level Smalltalk code. We also show how we can bootstrap with minimal effort two other languages (Pharo and MetaTalk) with similar execution semantics but different object models.
@InProceedings{Onward!15p183,
author = {Guillermo Polito and Stéphane Ducasse and Noury Bouraqadi and Luc Fabresse},
title = {A Bootstrapping Infrastructure to Build and Extend Pharo-Like Languages},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {183--196},
doi = {},
year = {2015},
}
Onward! '15: "Virtualization Support for ..."
Virtualization Support for Dynamic Core Library Update
Guillermo Polito, Stéphane Ducasse, Noury Bouraqadi, Luc Fabresse, and Max Mattone (INRIA, France; École des Mines de Douai, France) Dynamically updating language runtime and core libraries such as collections and threading is challenging since the update mechanism uses such libraries at the same time that it modifies them. To tackle this challenge, we present Dy- namic Core Library Update (DCU) as an extension of Dy- namic Software Update (DSU) and our approach based on a virtualization architecture. Our solution supports the up- date of core libraries as any other normal library, avoiding the circular dependencies between the updater and the core libraries. Our benchmarks show that there is no evident per- formance overhead in comparison with a default execution. Finally, we show that our approach can be applied to real life scenario by introducing a critical update inside a web application with 20 simulated concurrent users.
@InProceedings{Onward!15p211,
author = {Guillermo Polito and Stéphane Ducasse and Noury Bouraqadi and Luc Fabresse and Max Mattone},
title = {Virtualization Support for Dynamic Core Library Update},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {211--223},
doi = {},
year = {2015},
}
|
|
| Gall, Harald C. |
Onward! '15: "Runtime Metric Meets Developer: ..."
Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback
Jürgen Cito, Philipp Leitner, Harald C. Gall, Aryan Dadashi, Anne Keller, and Andreas Roth (University of Zurich, Switzerland; SAP, Germany) A unifying theme of many ongoing trends in software engineering is a blurring of the boundaries between building and operating software products. In this paper, we explore what we consider to be the logical next step in this succession: integrating runtime monitoring data from production deployments of the software into the tools developers utilize in their daily workflows (i.e., IDEs) to enable tighter feedback loops. We refer to this notion as feedback-driven development (FDD). This more abstract FDD concept can be instantiated in various ways, ranging from IDE plugins that implement feedback-driven refactoring and code optimization to plugins that predict performance and cost implications of code changes prior to even deploying the new version of the soft- ware. We demonstrate existing proof-of-concept realizations of these ideas and illustrate our vision of the future of FDD and cloud-based software development in general. Further, we discuss the major challenges that need to be solved be- fore FDD can achieve mainstream adoption.
@InProceedings{Onward!15p14,
author = {Jürgen Cito and Philipp Leitner and Harald C. Gall and Aryan Dadashi and Anne Keller and Andreas Roth},
title = {Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {14--27},
doi = {},
year = {2015},
}
|
|
 |
Garbervetsky, Diego |
Onward! '15: "Towards Fully Reflective Environments ..."
Towards Fully Reflective Environments
Guido Chari, Diego Garbervetsky, Stefan Marr, and Stéphane Ducasse (CONICET, Argentina; University of Buenos Aires, Argentina; INRIA, France) Modern development environments promote live programming (LP) mechanisms because it enhances the development experience by providing instantaneous feedback and interaction with live objects. LP is typically supported with advanced reflective techniques within dynamic languages. These languages run on top of Virtual Machines (VMs) that are built in a static manner so that most of their components are bound at compile time. As a consequence, VM developers are forced to work using the traditional edit-compile-run cycle, even when they are designing LP-supporting environments. In this paper we explore the idea of bringing LP techniques to the VM domain for improving their observability, evolution and adaptability at run-time. We define the notion of fully reflective execution environments (EEs), systems that provide reflection not only at the application level but also at the level of the VM. We characterize such systems, propose a design, and present Mate v1, a prototypical implementation. Based on our prototype, we analyze the feasibility and applicability of incorporating reflective capabilities into different parts of EEs. Furthermore, the evaluation demonstrates the opportunities such reflective capabilities provide for unanticipated dynamic adaptation scenarios, benefiting thus, a wider range of users.
@InProceedings{Onward!15p240,
author = {Guido Chari and Diego Garbervetsky and Stefan Marr and Stéphane Ducasse},
title = {Towards Fully Reflective Environments},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {240--253},
doi = {},
year = {2015},
}
|
| Gillick, Amy |
Onward! '15: "Musiplectics: Computational ..."
Musiplectics: Computational Assessment of the Complexity of Music Scores
Ethan Holder, Eli Tilevich, and Amy Gillick (Virginia Tech, USA) In the Western classical tradition, musicians play music from notated sheet music, called a score. When playing music from a score, a musician translates its visual symbols into sequences of instrument-specific physical motions. Hence, a music score's overall complexity represents a sum of the cognitive and mechanical acuity required for its performance. For a given instrument, different notes, intervals, articulations, dynamics, key signatures, and tempo represent dissimilar levels of difficulty, which vary depending on the performer's proficiency. Individual musicians embrace this tenet, but may disagree about the degrees of difficulty. This paper introduces musiplectics (musiplectics = music + plectics, Greek for the study of complexity), a systematic and objective approach to computational assessment of the complexity of a music score for any instrument. Musiplectics defines computing paradigms for automatically and accurately calculating the complexity of playing a music score on a given instrument. The core concept codifies a two-phase process. First, music experts rank the relative difficulty of individual musical components (e.g., notes, intervals, dynamics, etc.) for different playing proficiencies and instruments. Second, a computing engine automatically applies this ranking to music scores and calculates their respective complexity. As a proof of concept of musiplectics, we present an automated, Web-based application called Musical Complexity Scoring (MCS) for music educators and performers. Musiplectics can engender the creation of practical computing tools for objective and expeditious assessment of a music score's suitability for the abilities of intended performers.
@InProceedings{Onward!15p107,
author = {Ethan Holder and Eli Tilevich and Amy Gillick},
title = {Musiplectics: Computational Assessment of the Complexity of Music Scores},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {107--120},
doi = {},
year = {2015},
}
Info
|
|
| Gîrba, Tudor |
Onward! '15: "The Moldable Inspector ..."
The Moldable Inspector
Andrei Chiş, Oscar Nierstrasz, Aliaksei Syrel, and Tudor Gîrba (University of Bern, Switzerland; tudorgirba.com, Switzerland) Object inspectors are an essential category of tools that allow developers to comprehend the run-time of object-oriented systems. Traditional object inspectors favor a generic view that focuses on the low-level details of the state of single objects. Based on 16 interviews with software developers and a follow-up survey with 62 respondents we identified a need for object inspectors that support different high-level ways to visualize and explore objects, depending on both the object and the current developer need. We propose the Moldable Inspector, a novel inspector model that enables developers to adapt the inspection workflow to suit their immediate needs by making the inspection context explicit, providing multiple interchangeable domain-specific views for each object, and supporting a workflow that groups together multiple levels of connected objects. We show that the Moldable Inspector can address multiple kinds of development needs involving a wide range of objects.
@InProceedings{Onward!15p44,
author = {Andrei Chiş and Oscar Nierstrasz and Aliaksei Syrel and Tudor Gîrba},
title = {The Moldable Inspector},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {44--60},
doi = {},
year = {2015},
}
Info
|
|
| Grewe, Sylvia |
Onward! '15: "Type Systems for the Masses: ..."
Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers
Sylvia Grewe, Sebastian Erdweg, Pascal Wittmann, and Mira Mezini (TU Darmstadt, Germany; Lancaster University, UK) The correct definition and implementation of non-trivial type systems is difficult and requires expert knowledge, which is not available to developers of domain-specific languages (DSLs) in practice. We propose Veritas, a workbench that simplifies the development of sound type systems. Veritas provides a single, high-level specification language for type systems, from which it automatically tries to derive soundness proofs and efficient and correct type-checking algorithms. For verification, Veritas combines off-the-shelf automated first-order theorem provers with automated proof strategies specific to type systems. For deriving efficient type checkers, Veritas provides a collection of optimization strategies whose applicability to a given type system is checked through verification on a case-by-case basis. We have developed a prototypical implementation of Veritas and used it to verify type soundness of the simply-typed lambda calculus and of parts of typed SQL. Our experience suggests that many of the individual verification steps can be automated and, in particular, that a high degree of automation is possible for type systems of DSLs.
@InProceedings{Onward!15p137,
author = {Sylvia Grewe and Sebastian Erdweg and Pascal Wittmann and Mira Mezini},
title = {Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {137--150},
doi = {},
year = {2015},
}
|
|
| Henning, Johannes |
Onward! '15: "Columnar Objects: Improving ..."
Columnar Objects: Improving the Performance of Analytical Applications
Toni Mattis, Johannes Henning, Patrick Rein, Robert Hirschfeld, and Malte Appeltauer (HPI, Germany; SAP, Germany) Growing volumes of data increase the demand to use it in analytical applications to make informed decisions. Unfortunately, object-oriented runtimes experience performance problems when dealing with large data volumes. Similar problems have been addressed by column-oriented in-memory databases, whose memory layout is tailored to analytical workloads. As a result, data storage and processing are often delegated to such a database. However, the more domain logic is moved to this separate system, the more benefits of object-orientation are lost. We propose modifications to dynamic object-oriented runtimes to store collections of objects in a column-oriented memory layout and leverage a jit to take advantage of the adjusted layout by mapping object traversal to array operations. We implemented our concept in PyPy, a Python interpreter equipped with a tracing jit. Finally, we show that analytical algorithms, expressed through object-oriented code, are up to three times faster due to our optimizations, without substantially impairing the paradigm. Hopefully, extending these concepts will mitigate some problems originating from the paradigm mismatch between object-oriented runtimes and databases.
@InProceedings{Onward!15p197,
author = {Toni Mattis and Johannes Henning and Patrick Rein and Robert Hirschfeld and Malte Appeltauer},
title = {Columnar Objects: Improving the Performance of Analytical Applications},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {197--210},
doi = {},
year = {2015},
}
|
|
| Hirschfeld, Robert |
Onward! '15: "Columnar Objects: Improving ..."
Columnar Objects: Improving the Performance of Analytical Applications
Toni Mattis, Johannes Henning, Patrick Rein, Robert Hirschfeld, and Malte Appeltauer (HPI, Germany; SAP, Germany) Growing volumes of data increase the demand to use it in analytical applications to make informed decisions. Unfortunately, object-oriented runtimes experience performance problems when dealing with large data volumes. Similar problems have been addressed by column-oriented in-memory databases, whose memory layout is tailored to analytical workloads. As a result, data storage and processing are often delegated to such a database. However, the more domain logic is moved to this separate system, the more benefits of object-orientation are lost. We propose modifications to dynamic object-oriented runtimes to store collections of objects in a column-oriented memory layout and leverage a jit to take advantage of the adjusted layout by mapping object traversal to array operations. We implemented our concept in PyPy, a Python interpreter equipped with a tracing jit. Finally, we show that analytical algorithms, expressed through object-oriented code, are up to three times faster due to our optimizations, without substantially impairing the paradigm. Hopefully, extending these concepts will mitigate some problems originating from the paradigm mismatch between object-oriented runtimes and databases.
@InProceedings{Onward!15p197,
author = {Toni Mattis and Johannes Henning and Patrick Rein and Robert Hirschfeld and Malte Appeltauer},
title = {Columnar Objects: Improving the Performance of Analytical Applications},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {197--210},
doi = {},
year = {2015},
}
|
|
| Holder, Ethan |
Onward! '15: "Musiplectics: Computational ..."
Musiplectics: Computational Assessment of the Complexity of Music Scores
Ethan Holder, Eli Tilevich, and Amy Gillick (Virginia Tech, USA) In the Western classical tradition, musicians play music from notated sheet music, called a score. When playing music from a score, a musician translates its visual symbols into sequences of instrument-specific physical motions. Hence, a music score's overall complexity represents a sum of the cognitive and mechanical acuity required for its performance. For a given instrument, different notes, intervals, articulations, dynamics, key signatures, and tempo represent dissimilar levels of difficulty, which vary depending on the performer's proficiency. Individual musicians embrace this tenet, but may disagree about the degrees of difficulty. This paper introduces musiplectics (musiplectics = music + plectics, Greek for the study of complexity), a systematic and objective approach to computational assessment of the complexity of a music score for any instrument. Musiplectics defines computing paradigms for automatically and accurately calculating the complexity of playing a music score on a given instrument. The core concept codifies a two-phase process. First, music experts rank the relative difficulty of individual musical components (e.g., notes, intervals, dynamics, etc.) for different playing proficiencies and instruments. Second, a computing engine automatically applies this ranking to music scores and calculates their respective complexity. As a proof of concept of musiplectics, we present an automated, Web-based application called Musical Complexity Scoring (MCS) for music educators and performers. Musiplectics can engender the creation of practical computing tools for objective and expeditious assessment of a music score's suitability for the abilities of intended performers.
@InProceedings{Onward!15p107,
author = {Ethan Holder and Eli Tilevich and Amy Gillick},
title = {Musiplectics: Computational Assessment of the Complexity of Music Scores},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {107--120},
doi = {},
year = {2015},
}
Info
|
|
| Izmaylova, Anastasia |
Onward! '15: "One Parser to Rule Them All ..."
One Parser to Rule Them All
Ali Afroozeh and Anastasia Izmaylova (CWI, Netherlands) Despite the long history of research in parsing, constructing parsers for real programming languages remains a difficult and painful task. In the last decades, different parser generators emerged to allow the construction of parsers from a BNF-like specification. However, still today, many parsers are handwritten, or are only partly generated, and include various hacks to deal with different peculiarities in programming languages. The main problem is that current declarative syntax definition techniques are based on pure context-free grammars, while many constructs found in programming languages require context information. In this paper we propose a parsing framework that embraces context information in its core. Our framework is based on data-dependent grammars, which extend context-free grammars with arbitrary computation, variable binding and constraints. We present an implementation of our framework on top of the Generalized LL (GLL) parsing algorithm, and show how common idioms in syntax of programming languages such as (1) lexical disambiguation filters, (2) operator precedence, (3) indentation-sensitive rules, and (4) conditional preprocessor directives can be mapped to data-dependent grammars. We demonstrate the initial experience with our framework, by parsing more than 20000 Java, C#, Haskell, and OCaml source files.
@InProceedings{Onward!15p151,
author = {Ali Afroozeh and Anastasia Izmaylova},
title = {One Parser to Rule Them All},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {151--170},
doi = {},
year = {2015},
}
Info
|
|
 |
Jackson, Daniel |
Onward! '15: "Towards a Theory of Conceptual ..."
Towards a Theory of Conceptual Design for Software
Daniel Jackson (Massachusetts Institute of Technology, USA) Concepts are the building blocks of software systems. They are not just subjective mental constructs, but are objective features of a system's design: increments of functionality that were consciously introduced by a designer to serve particular purposes. This essay argues for viewing the design of software in terms of concepts, with their invention (or adoption) and refinement as the central activity of software design. A family of products can be characterized by arranging concepts in a dependence graph from which coherent concept subsets can be extracted. Just as bugs can be found in the code of a function prior to testing by reviewing the programmer's argument for its correctness, so flaws can be found in a software design by reviewing an argument by the designer. This argument consists of providing, for each concept, a single compelling purpose, and demonstrating how the concept fulfills the purpose with an archetypal scenario called an 'operational principle'. Some simple conditions (primarily in the relationship between concepts and their purposes) can then be applied to reveal flaws in the conceptual design.
@InProceedings{Onward!15p282,
author = {Daniel Jackson},
title = {Towards a Theory of Conceptual Design for Software},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {282--296},
doi = {},
year = {2015},
}
|
| Kay, Alan |
Onward! '15: "The Cuneiform Tablets of 2015 ..."
The Cuneiform Tablets of 2015
Long Tien Nguyen and Alan Kay (University of California at Los Angeles, USA; Viewpoints Research Institute, USA) We discuss the problem of running today's software decades, centuries, or even millennia into the future.
@InProceedings{Onward!15p297,
author = {Long Tien Nguyen and Alan Kay},
title = {The Cuneiform Tablets of 2015},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {297--307},
doi = {},
year = {2015},
}
|
|
| Keller, Anne |
Onward! '15: "Runtime Metric Meets Developer: ..."
Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback
Jürgen Cito, Philipp Leitner, Harald C. Gall, Aryan Dadashi, Anne Keller, and Andreas Roth (University of Zurich, Switzerland; SAP, Germany) A unifying theme of many ongoing trends in software engineering is a blurring of the boundaries between building and operating software products. In this paper, we explore what we consider to be the logical next step in this succession: integrating runtime monitoring data from production deployments of the software into the tools developers utilize in their daily workflows (i.e., IDEs) to enable tighter feedback loops. We refer to this notion as feedback-driven development (FDD). This more abstract FDD concept can be instantiated in various ways, ranging from IDE plugins that implement feedback-driven refactoring and code optimization to plugins that predict performance and cost implications of code changes prior to even deploying the new version of the soft- ware. We demonstrate existing proof-of-concept realizations of these ideas and illustrate our vision of the future of FDD and cloud-based software development in general. Further, we discuss the major challenges that need to be solved be- fore FDD can achieve mainstream adoption.
@InProceedings{Onward!15p14,
author = {Jürgen Cito and Philipp Leitner and Harald C. Gall and Aryan Dadashi and Anne Keller and Andreas Roth},
title = {Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {14--27},
doi = {},
year = {2015},
}
|
|
| Kell, Stephen |
Onward! '15: "Towards a Dynamic Object Model ..."
Towards a Dynamic Object Model within Unix Processes
Stephen Kell (University of Cambridge, UK) Programmers face much complexity from the co-existence of "native" (Unix-like) and virtual machine (VM) "managed" run-time environments. Rather than having VMs replace Unix processes, we investigate whether it makes sense for the latter to "become VMs", by evolving Unix's user-level services to subsume those of VMs. We survey the (little-understood) VM-like features in modern Unix, noting common shortcomings: a lack of semantic metadata ("type information") and the inability to bind from objects "back" to their metadata. We describe the design and implementation of a system, liballocs, which adds these capabilities in a highly compatible way, and explore its consequences.
@InProceedings{Onward!15p224,
author = {Stephen Kell},
title = {Towards a Dynamic Object Model within Unix Processes},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {224--239},
doi = {},
year = {2015},
}
|
|
| Krishnamurthi, Shriram |
Onward! '15: "Slimming Languages by Reducing ..."
Slimming Languages by Reducing Sugar: A Case for Semantics-Altering Transformations
Junsong Li, Justin Pombrio, Joe Gibbs Politz, and Shriram Krishnamurthi (Brown University, USA) Splitting a language into a core language and a desugaring function makes it possible to produce tractable semantics for real-world languages. It does so by pushing much of the language's complexity into desugaring. This, however, produces large and unwieldy core programs, which has proven to be a significant obstacle to actual use of these semantics. In this paper we analyze this problem for a semantics of JavaScript. We show that much of the bloat is *semantic bloat*: a consequence of the language's rich semantics. We demonstrate how assumptions about language use can confine this bloat, and codify these through several transformations that, in general, do not preserve the language's semantics. We experimentally demonstrate the effectiveness of these transformations. Finally, we discuss the implications of this work on language design and structure.
@InProceedings{Onward!15p90,
author = {Junsong Li and Justin Pombrio and Joe Gibbs Politz and Shriram Krishnamurthi},
title = {Slimming Languages by Reducing Sugar: A Case for Semantics-Altering Transformations},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {90--106},
doi = {},
year = {2015},
}
|
|
 |
Leitner, Philipp |
Onward! '15: "Runtime Metric Meets Developer: ..."
Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback
Jürgen Cito, Philipp Leitner, Harald C. Gall, Aryan Dadashi, Anne Keller, and Andreas Roth (University of Zurich, Switzerland; SAP, Germany) A unifying theme of many ongoing trends in software engineering is a blurring of the boundaries between building and operating software products. In this paper, we explore what we consider to be the logical next step in this succession: integrating runtime monitoring data from production deployments of the software into the tools developers utilize in their daily workflows (i.e., IDEs) to enable tighter feedback loops. We refer to this notion as feedback-driven development (FDD). This more abstract FDD concept can be instantiated in various ways, ranging from IDE plugins that implement feedback-driven refactoring and code optimization to plugins that predict performance and cost implications of code changes prior to even deploying the new version of the soft- ware. We demonstrate existing proof-of-concept realizations of these ideas and illustrate our vision of the future of FDD and cloud-based software development in general. Further, we discuss the major challenges that need to be solved be- fore FDD can achieve mainstream adoption.
@InProceedings{Onward!15p14,
author = {Jürgen Cito and Philipp Leitner and Harald C. Gall and Aryan Dadashi and Anne Keller and Andreas Roth},
title = {Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {14--27},
doi = {},
year = {2015},
}
|
| Li, Junsong |
Onward! '15: "Slimming Languages by Reducing ..."
Slimming Languages by Reducing Sugar: A Case for Semantics-Altering Transformations
Junsong Li, Justin Pombrio, Joe Gibbs Politz, and Shriram Krishnamurthi (Brown University, USA) Splitting a language into a core language and a desugaring function makes it possible to produce tractable semantics for real-world languages. It does so by pushing much of the language's complexity into desugaring. This, however, produces large and unwieldy core programs, which has proven to be a significant obstacle to actual use of these semantics. In this paper we analyze this problem for a semantics of JavaScript. We show that much of the bloat is *semantic bloat*: a consequence of the language's rich semantics. We demonstrate how assumptions about language use can confine this bloat, and codify these through several transformations that, in general, do not preserve the language's semantics. We experimentally demonstrate the effectiveness of these transformations. Finally, we discuss the implications of this work on language design and structure.
@InProceedings{Onward!15p90,
author = {Junsong Li and Justin Pombrio and Joe Gibbs Politz and Shriram Krishnamurthi},
title = {Slimming Languages by Reducing Sugar: A Case for Semantics-Altering Transformations},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {90--106},
doi = {},
year = {2015},
}
|
|
| Lorenz, David H. |
Onward! '15: "Separation of Powers in the ..."
Separation of Powers in the Cloud: Where Applications and Users Become Peers
David H. Lorenz and Boaz Rosenan (Open University, Israel; Technion, Israel; University of Haifa, Israel) We challenge the widely accepted practice that web applications must be trusted with user data. We present an alternative model based on logic programming, where users and applications are equal peers in a shared cloud environment. User data is represented as a set of facts. The application is represented as a set of rules defining how user data is to be processed, but is not given direct access to the data. This way, end users remain the owners of their own data, and are able to determine who can see it and who can modify it. For concreteness, we define a data representation and query language, named Cloudlog, for a new family of deductive databases, named NoDatalog. We add access control to the language for guaranteeing that the rules provided by the application cannot change the choices made by users. We demonstrate how business logic can be expressed in Cloudlog, and discuss how an efficient Cloudlog-based database can be implemented.
@InProceedings{Onward!15p76,
author = {David H. Lorenz and Boaz Rosenan},
title = {Separation of Powers in the Cloud: Where Applications and Users Become Peers},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {76--89},
doi = {},
year = {2015},
}
|
|
| Marr, Stefan |
Onward! '15: "Towards Fully Reflective Environments ..."
Towards Fully Reflective Environments
Guido Chari, Diego Garbervetsky, Stefan Marr, and Stéphane Ducasse (CONICET, Argentina; University of Buenos Aires, Argentina; INRIA, France) Modern development environments promote live programming (LP) mechanisms because it enhances the development experience by providing instantaneous feedback and interaction with live objects. LP is typically supported with advanced reflective techniques within dynamic languages. These languages run on top of Virtual Machines (VMs) that are built in a static manner so that most of their components are bound at compile time. As a consequence, VM developers are forced to work using the traditional edit-compile-run cycle, even when they are designing LP-supporting environments. In this paper we explore the idea of bringing LP techniques to the VM domain for improving their observability, evolution and adaptability at run-time. We define the notion of fully reflective execution environments (EEs), systems that provide reflection not only at the application level but also at the level of the VM. We characterize such systems, propose a design, and present Mate v1, a prototypical implementation. Based on our prototype, we analyze the feasibility and applicability of incorporating reflective capabilities into different parts of EEs. Furthermore, the evaluation demonstrates the opportunities such reflective capabilities provide for unanticipated dynamic adaptation scenarios, benefiting thus, a wider range of users.
@InProceedings{Onward!15p240,
author = {Guido Chari and Diego Garbervetsky and Stefan Marr and Stéphane Ducasse},
title = {Towards Fully Reflective Environments},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {240--253},
doi = {},
year = {2015},
}
Onward! '15: "Just-in-Time Data Structures ..."
Just-in-Time Data Structures
Mattias De Wael, Stefan Marr, Joeri De Koster, Jennifer B. Sartor, and Wolfgang De Meuter (Vrije Universiteit Brussel, Belgium; INRIA, France; Ghent University, Belgium) Today, software engineering practices focus on finding the single ``right'' data representation for a program. The ``right'' data representation, however, might not exist: changing the representation of an object during program execution can be better in terms of performance. To this end we introduce Just-in-Time Data Structures, which enable representation changes at runtime, based on declarative input from a performance expert programmer. Just-in-Time Data Structures are an attempt to shift the focus from finding the ``right'' data structure to finding the ``right'' sequence of data representations. We present JitDS, a programming language to develop such Just-in-Time Data Structures. Further, we show two example programs that benefit from changing the representation at runtime.
@InProceedings{Onward!15p61,
author = {Mattias De Wael and Stefan Marr and Joeri De Koster and Jennifer B. Sartor and Wolfgang De Meuter},
title = {Just-in-Time Data Structures},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {61--75},
doi = {},
year = {2015},
}
Info
|
|
| Mattis, Toni |
Onward! '15: "Columnar Objects: Improving ..."
Columnar Objects: Improving the Performance of Analytical Applications
Toni Mattis, Johannes Henning, Patrick Rein, Robert Hirschfeld, and Malte Appeltauer (HPI, Germany; SAP, Germany) Growing volumes of data increase the demand to use it in analytical applications to make informed decisions. Unfortunately, object-oriented runtimes experience performance problems when dealing with large data volumes. Similar problems have been addressed by column-oriented in-memory databases, whose memory layout is tailored to analytical workloads. As a result, data storage and processing are often delegated to such a database. However, the more domain logic is moved to this separate system, the more benefits of object-orientation are lost. We propose modifications to dynamic object-oriented runtimes to store collections of objects in a column-oriented memory layout and leverage a jit to take advantage of the adjusted layout by mapping object traversal to array operations. We implemented our concept in PyPy, a Python interpreter equipped with a tracing jit. Finally, we show that analytical algorithms, expressed through object-oriented code, are up to three times faster due to our optimizations, without substantially impairing the paradigm. Hopefully, extending these concepts will mitigate some problems originating from the paradigm mismatch between object-oriented runtimes and databases.
@InProceedings{Onward!15p197,
author = {Toni Mattis and Johannes Henning and Patrick Rein and Robert Hirschfeld and Malte Appeltauer},
title = {Columnar Objects: Improving the Performance of Analytical Applications},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {197--210},
doi = {},
year = {2015},
}
|
|
| Mattone, Max |
Onward! '15: "Virtualization Support for ..."
Virtualization Support for Dynamic Core Library Update
Guillermo Polito, Stéphane Ducasse, Noury Bouraqadi, Luc Fabresse, and Max Mattone (INRIA, France; École des Mines de Douai, France) Dynamically updating language runtime and core libraries such as collections and threading is challenging since the update mechanism uses such libraries at the same time that it modifies them. To tackle this challenge, we present Dy- namic Core Library Update (DCU) as an extension of Dy- namic Software Update (DSU) and our approach based on a virtualization architecture. Our solution supports the up- date of core libraries as any other normal library, avoiding the circular dependencies between the updater and the core libraries. Our benchmarks show that there is no evident per- formance overhead in comparison with a default execution. Finally, we show that our approach can be applied to real life scenario by introducing a critical update inside a web application with 20 simulated concurrent users.
@InProceedings{Onward!15p211,
author = {Guillermo Polito and Stéphane Ducasse and Noury Bouraqadi and Luc Fabresse and Max Mattone},
title = {Virtualization Support for Dynamic Core Library Update},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {211--223},
doi = {},
year = {2015},
}
|
|
| Mezini, Mira |
Onward! '15: "Type Systems for the Masses: ..."
Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers
Sylvia Grewe, Sebastian Erdweg, Pascal Wittmann, and Mira Mezini (TU Darmstadt, Germany; Lancaster University, UK) The correct definition and implementation of non-trivial type systems is difficult and requires expert knowledge, which is not available to developers of domain-specific languages (DSLs) in practice. We propose Veritas, a workbench that simplifies the development of sound type systems. Veritas provides a single, high-level specification language for type systems, from which it automatically tries to derive soundness proofs and efficient and correct type-checking algorithms. For verification, Veritas combines off-the-shelf automated first-order theorem provers with automated proof strategies specific to type systems. For deriving efficient type checkers, Veritas provides a collection of optimization strategies whose applicability to a given type system is checked through verification on a case-by-case basis. We have developed a prototypical implementation of Veritas and used it to verify type soundness of the simply-typed lambda calculus and of parts of typed SQL. Our experience suggests that many of the individual verification steps can be automated and, in particular, that a high degree of automation is possible for type systems of DSLs.
@InProceedings{Onward!15p137,
author = {Sylvia Grewe and Sebastian Erdweg and Pascal Wittmann and Mira Mezini},
title = {Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {137--150},
doi = {},
year = {2015},
}
Onward! '15: "Towards Secure Integration ..."
Towards Secure Integration of Cryptographic Software
Steven Arzt, Sarah Nadi, Karim Ali, Eric Bodden, Sebastian Erdweg, and Mira Mezini (TU Darmstadt, Germany) While cryptography is now readily available to everyone and can, provably, protect private information from attackers, we still frequently hear about major data leakages, many of which are due to improper use of cryptographic mechanisms. The problem is that many application developers are not cryptographic experts. Even though high-quality cryptographic APIs are widely available, programmers often select the wrong algorithms or misuse APIs due to a lack of understanding. Such issues arise with both simple operations such as encryption as well as with complex secure communication protocols such as SSL. In this paper, we provide a long-term solution that helps application developers integrate cryptographic components correctly and securely by bridging the gap between cryptographers and application developers. Our solution consists of a software product line (with an underlying feature model) that automatically identifies the correct cryptographic algorithms to use, based on the developer's answers to high-level questions in non-expert terminology. Each feature (i.e., cryptographic algorithm) maps into corresponding Java code and a usage protocol describing API restrictions. By composing the user's selected features, we automatically synthesize a secure code blueprint and a usage protocol that corresponds to the selected usage scenario. Since the developer may change the application code over time, we use the usage protocols to statically analyze the program and ensure that the correct use of the API is not violated over time.
@InProceedings{Onward!15p1,
author = {Steven Arzt and Sarah Nadi and Karim Ali and Eric Bodden and Sebastian Erdweg and Mira Mezini},
title = {Towards Secure Integration of Cryptographic Software},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {1--13},
doi = {},
year = {2015},
}
|
|
| Nadi, Sarah |
Onward! '15: "Towards Secure Integration ..."
Towards Secure Integration of Cryptographic Software
Steven Arzt, Sarah Nadi, Karim Ali, Eric Bodden, Sebastian Erdweg, and Mira Mezini (TU Darmstadt, Germany) While cryptography is now readily available to everyone and can, provably, protect private information from attackers, we still frequently hear about major data leakages, many of which are due to improper use of cryptographic mechanisms. The problem is that many application developers are not cryptographic experts. Even though high-quality cryptographic APIs are widely available, programmers often select the wrong algorithms or misuse APIs due to a lack of understanding. Such issues arise with both simple operations such as encryption as well as with complex secure communication protocols such as SSL. In this paper, we provide a long-term solution that helps application developers integrate cryptographic components correctly and securely by bridging the gap between cryptographers and application developers. Our solution consists of a software product line (with an underlying feature model) that automatically identifies the correct cryptographic algorithms to use, based on the developer's answers to high-level questions in non-expert terminology. Each feature (i.e., cryptographic algorithm) maps into corresponding Java code and a usage protocol describing API restrictions. By composing the user's selected features, we automatically synthesize a secure code blueprint and a usage protocol that corresponds to the selected usage scenario. Since the developer may change the application code over time, we use the usage protocols to statically analyze the program and ensure that the correct use of the API is not violated over time.
@InProceedings{Onward!15p1,
author = {Steven Arzt and Sarah Nadi and Karim Ali and Eric Bodden and Sebastian Erdweg and Mira Mezini},
title = {Towards Secure Integration of Cryptographic Software},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {1--13},
doi = {},
year = {2015},
}
|
|
| Nguyen, Long Tien |
Onward! '15: "The Cuneiform Tablets of 2015 ..."
The Cuneiform Tablets of 2015
Long Tien Nguyen and Alan Kay (University of California at Los Angeles, USA; Viewpoints Research Institute, USA) We discuss the problem of running today's software decades, centuries, or even millennia into the future.
@InProceedings{Onward!15p297,
author = {Long Tien Nguyen and Alan Kay},
title = {The Cuneiform Tablets of 2015},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {297--307},
doi = {},
year = {2015},
}
|
|
 |
Nierstrasz, Oscar |
Onward! '15: "The Moldable Inspector ..."
The Moldable Inspector
Andrei Chiş, Oscar Nierstrasz, Aliaksei Syrel, and Tudor Gîrba (University of Bern, Switzerland; tudorgirba.com, Switzerland) Object inspectors are an essential category of tools that allow developers to comprehend the run-time of object-oriented systems. Traditional object inspectors favor a generic view that focuses on the low-level details of the state of single objects. Based on 16 interviews with software developers and a follow-up survey with 62 respondents we identified a need for object inspectors that support different high-level ways to visualize and explore objects, depending on both the object and the current developer need. We propose the Moldable Inspector, a novel inspector model that enables developers to adapt the inspection workflow to suit their immediate needs by making the inspection context explicit, providing multiple interchangeable domain-specific views for each object, and supporting a workflow that groups together multiple levels of connected objects. We show that the Moldable Inspector can address multiple kinds of development needs involving a wide range of objects.
@InProceedings{Onward!15p44,
author = {Andrei Chiş and Oscar Nierstrasz and Aliaksei Syrel and Tudor Gîrba},
title = {The Moldable Inspector},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {44--60},
doi = {},
year = {2015},
}
Info
|
| Odersky, Martin |
Onward! '15: "Isolates, Channels, and Event ..."
Isolates, Channels, and Event Streams for Composable Distributed Programming
Aleksandar Prokopec and Martin Odersky (EPFL, Switzerland) The actor model has been a model of choice for building reliable distributed systems. On one hand, it ensures that message-processing is serialized within each actor, preserving the familiar sequential programming model. On the other hand, programs written in the actor model are location-transparent. The model is sufficiently low-level to express arbitrary message protocols. Composing these protocols is the key to high-level abstractions. Unfortunately, it is difficult to reuse or compose message protocols with actors. Reactive isolates, proposed in this paper, simplify protocol composition with first-class typed channels and event streams. We compare reactive isolates and the actor model on concrete programs. We identify obstacles for composition in the classic actor model, and show how to overcome them. We then show how to build reusable, composable distributed computing components in the new model.
@InProceedings{Onward!15p171,
author = {Aleksandar Prokopec and Martin Odersky},
title = {Isolates, Channels, and Event Streams for Composable Distributed Programming},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {171--182},
doi = {},
year = {2015},
}
|
|
| Petricek, Tomas |
Onward! '15: "Against a Universal Definition ..."
Against a Universal Definition of 'Type'
Tomas Petricek (University of Cambridge, UK) What is the definition of 'type'? Having a clear and precise answer to this question would avoid many misunderstandings and prevent meaningless discussions that arise from them. But having such clear and precise answer to this question would also hurt science, "hamper the growth of knowledge" and "deflect the course of investigation into narrow channels of things already understood". In this essay, I argue that not everything we work with needs to be precisely defined. There are many definitions used by different communities, but none of them applies universally. A brief excursion into philosophy of science shows that this is not just tolerable, but necessary for progress. Philosophy also suggests how we can think about this imprecise notion of type.
@InProceedings{Onward!15p254,
author = {Tomas Petricek},
title = {Against a Universal Definition of 'Type'},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {254--266},
doi = {},
year = {2015},
}
Info
|
|
| Polito, Guillermo |
Onward! '15: "A Bootstrapping Infrastructure ..."
A Bootstrapping Infrastructure to Build and Extend Pharo-Like Languages
Guillermo Polito, Stéphane Ducasse, Noury Bouraqadi, and Luc Fabresse (INRIA, France; École des Mines de Douai, France) Bootstrapping is well known in the context of compilers, where a bootstrapped compiler can compile its own source code. Bootstrapping is a beneficial engineering practice because it raises the level of abstraction of a program making it easier to understand, optimize, evolve, etc. Bootstrapping a reflective object-oriented language is however more challenging, as we need also to initialize the runtime of the language with its initial objects and classes besides writing its compiler. In this paper, we present a novel bootstrapping infrastructure for Pharo-like languages that allows us to easily extend and modify such languages. Our bootstrapping process relies on a first-class runtime. A first-class runtime is a meta-object that represents a program’s runtime and provides a MOP to easily load code into it and manipulate its objects. It decouples the virtual machine (VM) and language concerns by introducing a clear VM-language interface. Using this process, we show how we succeeded to bootstrap a Smalltalk-based language named Candle and then extend it with traits in less than 250 lines of high-level Smalltalk code. We also show how we can bootstrap with minimal effort two other languages (Pharo and MetaTalk) with similar execution semantics but different object models.
@InProceedings{Onward!15p183,
author = {Guillermo Polito and Stéphane Ducasse and Noury Bouraqadi and Luc Fabresse},
title = {A Bootstrapping Infrastructure to Build and Extend Pharo-Like Languages},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {183--196},
doi = {},
year = {2015},
}
Onward! '15: "Virtualization Support for ..."
Virtualization Support for Dynamic Core Library Update
Guillermo Polito, Stéphane Ducasse, Noury Bouraqadi, Luc Fabresse, and Max Mattone (INRIA, France; École des Mines de Douai, France) Dynamically updating language runtime and core libraries such as collections and threading is challenging since the update mechanism uses such libraries at the same time that it modifies them. To tackle this challenge, we present Dy- namic Core Library Update (DCU) as an extension of Dy- namic Software Update (DSU) and our approach based on a virtualization architecture. Our solution supports the up- date of core libraries as any other normal library, avoiding the circular dependencies between the updater and the core libraries. Our benchmarks show that there is no evident per- formance overhead in comparison with a default execution. Finally, we show that our approach can be applied to real life scenario by introducing a critical update inside a web application with 20 simulated concurrent users.
@InProceedings{Onward!15p211,
author = {Guillermo Polito and Stéphane Ducasse and Noury Bouraqadi and Luc Fabresse and Max Mattone},
title = {Virtualization Support for Dynamic Core Library Update},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {211--223},
doi = {},
year = {2015},
}
|
|
| Politz, Joe Gibbs |
Onward! '15: "Slimming Languages by Reducing ..."
Slimming Languages by Reducing Sugar: A Case for Semantics-Altering Transformations
Junsong Li, Justin Pombrio, Joe Gibbs Politz, and Shriram Krishnamurthi (Brown University, USA) Splitting a language into a core language and a desugaring function makes it possible to produce tractable semantics for real-world languages. It does so by pushing much of the language's complexity into desugaring. This, however, produces large and unwieldy core programs, which has proven to be a significant obstacle to actual use of these semantics. In this paper we analyze this problem for a semantics of JavaScript. We show that much of the bloat is *semantic bloat*: a consequence of the language's rich semantics. We demonstrate how assumptions about language use can confine this bloat, and codify these through several transformations that, in general, do not preserve the language's semantics. We experimentally demonstrate the effectiveness of these transformations. Finally, we discuss the implications of this work on language design and structure.
@InProceedings{Onward!15p90,
author = {Junsong Li and Justin Pombrio and Joe Gibbs Politz and Shriram Krishnamurthi},
title = {Slimming Languages by Reducing Sugar: A Case for Semantics-Altering Transformations},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {90--106},
doi = {},
year = {2015},
}
|
|
| Pombrio, Justin |
Onward! '15: "Slimming Languages by Reducing ..."
Slimming Languages by Reducing Sugar: A Case for Semantics-Altering Transformations
Junsong Li, Justin Pombrio, Joe Gibbs Politz, and Shriram Krishnamurthi (Brown University, USA) Splitting a language into a core language and a desugaring function makes it possible to produce tractable semantics for real-world languages. It does so by pushing much of the language's complexity into desugaring. This, however, produces large and unwieldy core programs, which has proven to be a significant obstacle to actual use of these semantics. In this paper we analyze this problem for a semantics of JavaScript. We show that much of the bloat is *semantic bloat*: a consequence of the language's rich semantics. We demonstrate how assumptions about language use can confine this bloat, and codify these through several transformations that, in general, do not preserve the language's semantics. We experimentally demonstrate the effectiveness of these transformations. Finally, we discuss the implications of this work on language design and structure.
@InProceedings{Onward!15p90,
author = {Junsong Li and Justin Pombrio and Joe Gibbs Politz and Shriram Krishnamurthi},
title = {Slimming Languages by Reducing Sugar: A Case for Semantics-Altering Transformations},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {90--106},
doi = {},
year = {2015},
}
|
|
| Prokopec, Aleksandar |
Onward! '15: "Isolates, Channels, and Event ..."
Isolates, Channels, and Event Streams for Composable Distributed Programming
Aleksandar Prokopec and Martin Odersky (EPFL, Switzerland) The actor model has been a model of choice for building reliable distributed systems. On one hand, it ensures that message-processing is serialized within each actor, preserving the familiar sequential programming model. On the other hand, programs written in the actor model are location-transparent. The model is sufficiently low-level to express arbitrary message protocols. Composing these protocols is the key to high-level abstractions. Unfortunately, it is difficult to reuse or compose message protocols with actors. Reactive isolates, proposed in this paper, simplify protocol composition with first-class typed channels and event streams. We compare reactive isolates and the actor model on concrete programs. We identify obstacles for composition in the classic actor model, and show how to overcome them. We then show how to build reusable, composable distributed computing components in the new model.
@InProceedings{Onward!15p171,
author = {Aleksandar Prokopec and Martin Odersky},
title = {Isolates, Channels, and Event Streams for Composable Distributed Programming},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {171--182},
doi = {},
year = {2015},
}
|
|
| Rein, Patrick |
Onward! '15: "Columnar Objects: Improving ..."
Columnar Objects: Improving the Performance of Analytical Applications
Toni Mattis, Johannes Henning, Patrick Rein, Robert Hirschfeld, and Malte Appeltauer (HPI, Germany; SAP, Germany) Growing volumes of data increase the demand to use it in analytical applications to make informed decisions. Unfortunately, object-oriented runtimes experience performance problems when dealing with large data volumes. Similar problems have been addressed by column-oriented in-memory databases, whose memory layout is tailored to analytical workloads. As a result, data storage and processing are often delegated to such a database. However, the more domain logic is moved to this separate system, the more benefits of object-orientation are lost. We propose modifications to dynamic object-oriented runtimes to store collections of objects in a column-oriented memory layout and leverage a jit to take advantage of the adjusted layout by mapping object traversal to array operations. We implemented our concept in PyPy, a Python interpreter equipped with a tracing jit. Finally, we show that analytical algorithms, expressed through object-oriented code, are up to three times faster due to our optimizations, without substantially impairing the paradigm. Hopefully, extending these concepts will mitigate some problems originating from the paradigm mismatch between object-oriented runtimes and databases.
@InProceedings{Onward!15p197,
author = {Toni Mattis and Johannes Henning and Patrick Rein and Robert Hirschfeld and Malte Appeltauer},
title = {Columnar Objects: Improving the Performance of Analytical Applications},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {197--210},
doi = {},
year = {2015},
}
|
|
| Rosenan, Boaz |
Onward! '15: "Separation of Powers in the ..."
Separation of Powers in the Cloud: Where Applications and Users Become Peers
David H. Lorenz and Boaz Rosenan (Open University, Israel; Technion, Israel; University of Haifa, Israel) We challenge the widely accepted practice that web applications must be trusted with user data. We present an alternative model based on logic programming, where users and applications are equal peers in a shared cloud environment. User data is represented as a set of facts. The application is represented as a set of rules defining how user data is to be processed, but is not given direct access to the data. This way, end users remain the owners of their own data, and are able to determine who can see it and who can modify it. For concreteness, we define a data representation and query language, named Cloudlog, for a new family of deductive databases, named NoDatalog. We add access control to the language for guaranteeing that the rules provided by the application cannot change the choices made by users. We demonstrate how business logic can be expressed in Cloudlog, and discuss how an efficient Cloudlog-based database can be implemented.
@InProceedings{Onward!15p76,
author = {David H. Lorenz and Boaz Rosenan},
title = {Separation of Powers in the Cloud: Where Applications and Users Become Peers},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {76--89},
doi = {},
year = {2015},
}
|
|
| Roth, Andreas |
Onward! '15: "Runtime Metric Meets Developer: ..."
Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback
Jürgen Cito, Philipp Leitner, Harald C. Gall, Aryan Dadashi, Anne Keller, and Andreas Roth (University of Zurich, Switzerland; SAP, Germany) A unifying theme of many ongoing trends in software engineering is a blurring of the boundaries between building and operating software products. In this paper, we explore what we consider to be the logical next step in this succession: integrating runtime monitoring data from production deployments of the software into the tools developers utilize in their daily workflows (i.e., IDEs) to enable tighter feedback loops. We refer to this notion as feedback-driven development (FDD). This more abstract FDD concept can be instantiated in various ways, ranging from IDE plugins that implement feedback-driven refactoring and code optimization to plugins that predict performance and cost implications of code changes prior to even deploying the new version of the soft- ware. We demonstrate existing proof-of-concept realizations of these ideas and illustrate our vision of the future of FDD and cloud-based software development in general. Further, we discuss the major challenges that need to be solved be- fore FDD can achieve mainstream adoption.
@InProceedings{Onward!15p14,
author = {Jürgen Cito and Philipp Leitner and Harald C. Gall and Aryan Dadashi and Anne Keller and Andreas Roth},
title = {Runtime Metric Meets Developer: Building Better Cloud Applications using Feedback},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {14--27},
doi = {},
year = {2015},
}
|
|
| Samimi, Hesam |
Onward! '15: "Constraints as a Design Pattern ..."
Constraints as a Design Pattern
Hesam Samimi, Alessandro Warth, Mahdi Eslamimehr, and Alan Borning (SAP Labs, USA; Viewpoints Research Institute, USA) Imperative programming has great merits. As the ubiquitous style, it is familiar, and its linear and step by step nature is favored by the human mind. Experienced programmers, however, are aware of its major flaw: it is easy for meanings to get lost in piles of code, making software hard to understand, extend, and debug. Constraint-based programming as an alternative has been observed to suffer much less from these flaws, where the "what" (the intention) is expressed rather than the "how" (the algorithm) in performing a computation. It is the job of the system to automatically achieve the intention through constraint solving. Sadly, poor performance and expressiveness has prevented this style from seeing widespread adoption. We propose a general programming model as a kind of a sweet spot between imperative and constraint-based programming. Our aim is to leverage many benefits of constraint-based programming such as understandability, behavioral modularity, extensibility, etc., in a practical way and without suffering the breakdown of the approach as with the traditional constraint-based paradigm. This model enforces a certain organization where at the top-level a program is simply composed of a set of constraints. However, the constraints aren't necessarily solved by an external entity, and the programmer uses imperative code to specify (1) how each constraint should be solved in isolation, and (2) how to combine individual solutions. We have implemented a tool called Sketchpad14 that incorporates this model in JavaScript, and built a number of realistic applications in it. In this paper we demonstrate the merits of our approach by comparing it with traditional imperative as well as constraint-based approaches.
@InProceedings{Onward!15p28,
author = {Hesam Samimi and Alessandro Warth and Mahdi Eslamimehr and Alan Borning},
title = {Constraints as a Design Pattern},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {28--43},
doi = {},
year = {2015},
}
Info
|
|
| Sartor, Jennifer B. |
Onward! '15: "Just-in-Time Data Structures ..."
Just-in-Time Data Structures
Mattias De Wael, Stefan Marr, Joeri De Koster, Jennifer B. Sartor, and Wolfgang De Meuter (Vrije Universiteit Brussel, Belgium; INRIA, France; Ghent University, Belgium) Today, software engineering practices focus on finding the single ``right'' data representation for a program. The ``right'' data representation, however, might not exist: changing the representation of an object during program execution can be better in terms of performance. To this end we introduce Just-in-Time Data Structures, which enable representation changes at runtime, based on declarative input from a performance expert programmer. Just-in-Time Data Structures are an attempt to shift the focus from finding the ``right'' data structure to finding the ``right'' sequence of data representations. We present JitDS, a programming language to develop such Just-in-Time Data Structures. Further, we show two example programs that benefit from changing the representation at runtime.
@InProceedings{Onward!15p61,
author = {Mattias De Wael and Stefan Marr and Joeri De Koster and Jennifer B. Sartor and Wolfgang De Meuter},
title = {Just-in-Time Data Structures},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {61--75},
doi = {},
year = {2015},
}
Info
|
|
| Syrel, Aliaksei |
Onward! '15: "The Moldable Inspector ..."
The Moldable Inspector
Andrei Chiş, Oscar Nierstrasz, Aliaksei Syrel, and Tudor Gîrba (University of Bern, Switzerland; tudorgirba.com, Switzerland) Object inspectors are an essential category of tools that allow developers to comprehend the run-time of object-oriented systems. Traditional object inspectors favor a generic view that focuses on the low-level details of the state of single objects. Based on 16 interviews with software developers and a follow-up survey with 62 respondents we identified a need for object inspectors that support different high-level ways to visualize and explore objects, depending on both the object and the current developer need. We propose the Moldable Inspector, a novel inspector model that enables developers to adapt the inspection workflow to suit their immediate needs by making the inspection context explicit, providing multiple interchangeable domain-specific views for each object, and supporting a workflow that groups together multiple levels of connected objects. We show that the Moldable Inspector can address multiple kinds of development needs involving a wide range of objects.
@InProceedings{Onward!15p44,
author = {Andrei Chiş and Oscar Nierstrasz and Aliaksei Syrel and Tudor Gîrba},
title = {The Moldable Inspector},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {44--60},
doi = {},
year = {2015},
}
Info
|
|
| Tilevich, Eli |
Onward! '15: "Musiplectics: Computational ..."
Musiplectics: Computational Assessment of the Complexity of Music Scores
Ethan Holder, Eli Tilevich, and Amy Gillick (Virginia Tech, USA) In the Western classical tradition, musicians play music from notated sheet music, called a score. When playing music from a score, a musician translates its visual symbols into sequences of instrument-specific physical motions. Hence, a music score's overall complexity represents a sum of the cognitive and mechanical acuity required for its performance. For a given instrument, different notes, intervals, articulations, dynamics, key signatures, and tempo represent dissimilar levels of difficulty, which vary depending on the performer's proficiency. Individual musicians embrace this tenet, but may disagree about the degrees of difficulty. This paper introduces musiplectics (musiplectics = music + plectics, Greek for the study of complexity), a systematic and objective approach to computational assessment of the complexity of a music score for any instrument. Musiplectics defines computing paradigms for automatically and accurately calculating the complexity of playing a music score on a given instrument. The core concept codifies a two-phase process. First, music experts rank the relative difficulty of individual musical components (e.g., notes, intervals, dynamics, etc.) for different playing proficiencies and instruments. Second, a computing engine automatically applies this ranking to music scores and calculates their respective complexity. As a proof of concept of musiplectics, we present an automated, Web-based application called Musical Complexity Scoring (MCS) for music educators and performers. Musiplectics can engender the creation of practical computing tools for objective and expeditious assessment of a music score's suitability for the abilities of intended performers.
@InProceedings{Onward!15p107,
author = {Ethan Holder and Eli Tilevich and Amy Gillick},
title = {Musiplectics: Computational Assessment of the Complexity of Music Scores},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {107--120},
doi = {},
year = {2015},
}
Info
|
|
| Torlak, Emina |
Onward! '15: "Toward Tool Support for Interactive ..."
Toward Tool Support for Interactive Synthesis
Shaon Barman, Rastislav Bodik, Satish Chandra, Emina Torlak, Arka Bhattacharya, and David Culler (University of California at Berkeley, USA; University of Washington, USA; Samsung Research, USA) Syntax-guided synthesis searches for an implementation of a given specification by exploring large spaces of candidate programs. Sketches reduce these search spaces, making synthesis more tractable, by predefining the structure of the desired implementation. Typically, this structure is obtained through human insight---this paper introduces a method for interactive, tool-supported discovery of such structure. The key idea is to decompose the specification into subcomputations such that the decomposition dictates the sketch. We rely on a readily obtainable specification that is nothing more than a finite set of sample input-output pairs or execution traces of the desired program. We introduce two complementary decomposition operators and demonstrate them on case studies. We find that our interactive methodology to discover structure extends the reach of computer-aided programming to problems that cannot be solved with synthesis alone.
@InProceedings{Onward!15p121,
author = {Shaon Barman and Rastislav Bodik and Satish Chandra and Emina Torlak and Arka Bhattacharya and David Culler},
title = {Toward Tool Support for Interactive Synthesis},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {121--136},
doi = {},
year = {2015},
}
|
|
| Warth, Alessandro |
Onward! '15: "Constraints as a Design Pattern ..."
Constraints as a Design Pattern
Hesam Samimi, Alessandro Warth, Mahdi Eslamimehr, and Alan Borning (SAP Labs, USA; Viewpoints Research Institute, USA) Imperative programming has great merits. As the ubiquitous style, it is familiar, and its linear and step by step nature is favored by the human mind. Experienced programmers, however, are aware of its major flaw: it is easy for meanings to get lost in piles of code, making software hard to understand, extend, and debug. Constraint-based programming as an alternative has been observed to suffer much less from these flaws, where the "what" (the intention) is expressed rather than the "how" (the algorithm) in performing a computation. It is the job of the system to automatically achieve the intention through constraint solving. Sadly, poor performance and expressiveness has prevented this style from seeing widespread adoption. We propose a general programming model as a kind of a sweet spot between imperative and constraint-based programming. Our aim is to leverage many benefits of constraint-based programming such as understandability, behavioral modularity, extensibility, etc., in a practical way and without suffering the breakdown of the approach as with the traditional constraint-based paradigm. This model enforces a certain organization where at the top-level a program is simply composed of a set of constraints. However, the constraints aren't necessarily solved by an external entity, and the programmer uses imperative code to specify (1) how each constraint should be solved in isolation, and (2) how to combine individual solutions. We have implemented a tool called Sketchpad14 that incorporates this model in JavaScript, and built a number of realistic applications in it. In this paper we demonstrate the merits of our approach by comparing it with traditional imperative as well as constraint-based approaches.
@InProceedings{Onward!15p28,
author = {Hesam Samimi and Alessandro Warth and Mahdi Eslamimehr and Alan Borning},
title = {Constraints as a Design Pattern},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {28--43},
doi = {},
year = {2015},
}
Info
|
|
| West, David M. |
Onward! '15: "The Cuban Software Revolution: ..."
The Cuban Software Revolution: 2016–2025
David M. West (Transcendence, USA) Presented as a work of fiction, this essay is about software development— how it has come to be what it is and what it might have been. The concept and metaphor of culture is used to frame the discussion. What might have been is presented as an approach named “Living System Design” and its practice in a fictional Cuba of the near future.
@InProceedings{Onward!15p267,
author = {David M. West},
title = {The Cuban Software Revolution: 2016–2025},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {267--281},
doi = {},
year = {2015},
}
|
|
| Wittmann, Pascal |
Onward! '15: "Type Systems for the Masses: ..."
Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers
Sylvia Grewe, Sebastian Erdweg, Pascal Wittmann, and Mira Mezini (TU Darmstadt, Germany; Lancaster University, UK) The correct definition and implementation of non-trivial type systems is difficult and requires expert knowledge, which is not available to developers of domain-specific languages (DSLs) in practice. We propose Veritas, a workbench that simplifies the development of sound type systems. Veritas provides a single, high-level specification language for type systems, from which it automatically tries to derive soundness proofs and efficient and correct type-checking algorithms. For verification, Veritas combines off-the-shelf automated first-order theorem provers with automated proof strategies specific to type systems. For deriving efficient type checkers, Veritas provides a collection of optimization strategies whose applicability to a given type system is checked through verification on a case-by-case basis. We have developed a prototypical implementation of Veritas and used it to verify type soundness of the simply-typed lambda calculus and of parts of typed SQL. Our experience suggests that many of the individual verification steps can be automated and, in particular, that a high degree of automation is possible for type systems of DSLs.
@InProceedings{Onward!15p137,
author = {Sylvia Grewe and Sebastian Erdweg and Pascal Wittmann and Mira Mezini},
title = {Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers},
booktitle = {Proc.\ Onward!},
publisher = {ACM},
pages = {137--150},
doi = {},
year = {2015},
}
|
64 authors
proc time: 0.82