Schedule

Abstracts

Graph drawing tools such as Graphviz provide a declarative interface for drawing graphs. Compared to visual interfaces, declarative ones allow automation at varying levels of granularity for both generation and editing. Such a declarative interface is often called a Domain Specific Language (DSL). However, a purely declarative interface imposes limits on extensibility: customizations unsupported by the DSL require extending the DSL and its implementation (C, Flex, and Bison in the case of Graphviz). This work explores graph drawing via a Domain Specific Embedded Language (DSEL) in Haskell. The goal is to support modern visualization needs such as color gradients and custom, scalable shapes while maintaining a semantic and syntactic simplicity akin to Graphviz's DSL. It's Haskell all the way down, meaning uniform extensibility and powerful abstraction via parametric and ad-hoc polymorphism and higher order functions. A force-based layout algorithm explores the efficacy of Functional Reactive Programming for practical applications. Color and shape representations explore connections between Functional Images and traditional vector-based shapes.

Declarative User Interfaces with Property Models

Modern high-quality user interfaces support a large set of features: propagating values between widgets appropriately, script recording and play back, enabling and disabling widgets to better support the user, etc. This functionality is typically not reusable, but is instead tediously implemented per user interface as ad-hoc code in the event handlers of user interface widgets. In addition to constituting a significant portion of most applications, code managing user interfaces is reported to have a high frequency of defects. We presents a declarative approach for programming user interfaces, where a large part of the functionality of a user interface is implemented as reusable generic algorithms. These algorithms are parametrized by a concise model of the essential properties of the data manipulated by a user interface. The approach achieves high level of reuse in code that implements user interfaces. We have observed a decrease of defects as a result of adopting the approach.

One step toward Proving Correctness in Procedural Languages: Automated Testing using Counter-example Search

A number of obstacles prevent proofs of correctness for existing software. One of the most ignored barriers is the proficiency of the existing programmer base with respect to proof literacy. Even if a superior language were immediately available, many programmers would be unable to exploit it due to limited familiarity with first-order logic and the proof development process. Unless and until a radical shift occurs, semantically-complex procedural languages will not be replaced, however correctness continues to grow more important. Programmers need an opportunity to develop logic skills even if proofs are not completed. To this end, an extension has been developed for existing procedural language test harnesses to allow predicates stating correct behavior of code. A heuristics-guided search for counter examples provides a demonstration for how a future proof engine might be integrated with existing test harnesses and, by simplifying test case creation, provides incentive to begin developing correctness skills.

Acumen: An environment for rapid prototyping of cyber-physical systems

Cyber-Physical Systems (CPS) are integrations of computation and physical processes. With the increase in the applications of embedded computing, scientists and engineers are building more cyber-physical systems, where software application operates in physical context. The design process of a cyber-physical system consists of a repeated cycle through specification, simulation, prototyping and production. Simulation can help reveal design flaw in a much earlier stage and with lower failure cost, thus is an essential part of CPS design. However, existing modeling and simulation approaches generally employ a formalism that is distant from what engineers naturally use to design and model physical systems. This creates an artificial difference between the core of the engineer's work and what the engineer needs to do to employ the available computing resources. We believe that we can make simulation much easier by bridging the gap between the user specification and the machine executable. To investigate the viability of this approach, we have built a simulation environment called Acumen. The centerpiece of Acumen is a physical description language called PhyDL. PhyDL allows the user to directly describe dynamic equations governing the system being modeled. A series of automatic transformations convert the high-level descriptions into a form that is directly machine executable. By raising the level of abstraction for the developer, we avoid many of the problems that limit the effectiveness of traditional approaches in modeling and simulation of cyber-physical systems.

On isomorphic data type transformations in functional programming

We explore a uniform data0centric upper ontology of computational entities, derived from first principles: a groupoid of isomorphisms between fundamental data types provides the ability to shift views of a given informational entity at will. An embedded higher order combinator language provides any-to-any encodings automatically. Applications range from emulating Turing-equivalent functional programming languages in terms of simple arithmetic operations to generation of random instances.

The VPP Verilog Preprocessor

This abstract is an overview of the design of VPP, a tool aimed at introducing powerful programming language constructs to the mainstream hardware design. The Verilog language consists of module definition and instantiation constructs augmented by a set of ad hoc extensions inspired by C (e.g. assignments and expressions). Additionally, Verilog has a set of generative constructs like parameterized modules, conditionals, and loops. Preprocessing allows us to extend Verilog in a disciplined and backward compatible manner

Nested Control Regions

(Slides) Today's highly networked world makes protecting privacy and integrity of sensitive data an important goal in software development. Static information flow control is a technique that uses programming language extensions to allow static checking of security constraints. In prior work, Myers has developed the JIF language, an extension of the Java language. JIF is able to use static, compile-time checking, to verify that sensitive information is not leaked to non-sensitive variables except through explicit declassification operators. In a dynamically extensible environment like a Java virtual machine, this approach is not sufficient. In this context, security annotations need to be retained to allow verification of security policies while loading code. Common mobile code formats like Java Byte Code are not suited well to this task, since verification can take a large amount of time. We propose a new mobile code format called Nested Control Regions (NCR). Its novel blend of high-level control structures and low-level code allows verification with a simple single-pass, linear-time algorithm. On top of NCR we implement security annotations based on the Distributed Label Model and show that it is possible to verify information flow incrementally in a single, linear-time pass while loading the mobile code.

Staged Monad Transformers for Faster Modular Interpreters

Monad transformers are a powerful abstraction mechanism for building customized interpreters from modular components. Unfortunately, this modularity comes at a steep runtime cost. In this paper we show how the runtime performance of monadic interpreters can be improved using staging. The key challenge to achieving this goal is applying staging in a modular manner so as to preserve the advantages of the original monad transformer method. We show that there is, indeed, a sensible notion of staged monad transformers that preserves this modularity. Just as a staged interpreter partially interprets a program and returns code to do the rest, a staged monadic computation runs parts of an effectful computation and returns code for the remainder. Precise control over running and deferring computations is achieved by providing staged counterparts to monadic operators and types, as well as a mapping between staged and unstaged computations. We show that these notions can be applied to several transformers, and use them to stage the core example in the original work. Experimental results confirm that the staged interpreters improve performance substantially for programs that use recursion, backtracking, and first-class continuations, but struggle with mutable references and lazy functions.

Tactic-Driven Synthesis of Global Search Algorithms for Constraint Satisfaction Problems

Efficient algorithms can often be synthesized by combining a high-level problem specification with a generic algorithm. Success of this approach depends on the availability of an appropriate algorithm theory and also instantiation of the operators of the generic algorithm to take advantage of the structure of particular problems. This talk consists of two parts. In the first part, we define algorithm theories for constraint satisfaction optimization problems. The constraint satisfaction optimization theory is used to synthesize programs for a number of common problems, including maximum segment sum problems. To derive efficient algorithms, the theory is extended to include dominance relations. The talk also suggests the use of dominance relations as the basis of a form of greedy algorithm for constraint satisfaction. The second part of the talk relates to the calculation of the various operators, including dominance relations. Often the problem is not so much carrying out the actual calculation as knowing where to start. For this reason we propose some tactics that might be useful in aiding the developer, in the form of patterns and pattern matching rules.

Gel: A Generic Extensible Language

Slides Both XML and Lisp have demonstrated the utility of generic syntax for expressing tree-structured data. But generic languages do not provide the syntactic richness of custom languages. Generic Expression Language (Gel) is a rich generic syntax that embodies many of the common syntactic conventions for operators, grouping and lists in widely-used languages. Prefix/infix operators are disambiguated by white-space, so that documents which violate common white-space conventions will not necessarily parse correctly with Gel.With some character replacements and adjusting for mismatch in operator precedence, Gel can extract meaningful structure from typical files in many languages, including Java, CSS, Smalltalk, and ANTLR grammars. This evaluation shows the expressive power of Gel, not that Gel can be used as a parser for existing languages. Gel is intended to serve as a generic language for creating composable domain specific languages.

New Foundations for OO Languages

Since the advent of high-level programming languages fifty years ago, computer scientists have compiled a deep body of research on program semantics and proof systems rooted in mathematical logic, most notably the lambda-calculus. This research has supported the development of an array of sophisticated statically-typed functional languages and a variety of logical frameworks for reasoning about functional programs. Unfortunately, these languages and frameworks are not well-suited to formalizing mainstream object-oriented (OO) programming languages. Neither the semantic models nor the type systems developed for structurally-typed functional languages are a good match to mainstream OO languages. In this talk, I will outline an approach to constructing more robust mathematical foundations for nominally typed object-oriented languages in the form of intelligble yet faithful denotional models. I am particularly interested in improving and extending Java 6 to support first-class generic types including an intuitively tractable formulation of wildcards.

Slice, Partition, and Reforest for Data Access and Distribution