Rhombus is a new language that is built on Racket. It offers the same kind of language extensibility as Racket itself, but using traditional (infix) notation. Although Rhombus is far from the first language to support Lisp-style macros without Lisp-style parentheses, Rhombus offers a novel synthesis of macro technology that is practical and expressive. A key element is the use of multiple binding spaces for context-specific sublanguages. For example, expressions and pattern-matching forms can use the same operators with different meanings and without creating conflicts. Context-sensitive bindings, in turn, facilitate a language design that reduces the notational distance between the core language and macro facilities. For example, repetitions can be defined and used in binding and expression contexts generally, which enables a smoother transition from programming to metaprogramming. Finally, since handling static information (such as types) is also a necessary part of growing macros beyond Lisp, Rhombus includes support in its expansion protocol for communicating static information among bindings and expressions. The Rhombus implementation demonstrates that all of these pieces can work together in a coherent and user-friendly language.

Theories of higher-order must-alias analysis, often under the guise of environment analysis, provide deep behavioral insight. But these theories-in particular those that are most insightful otherwise-can reason about recursion only in limited cases. This weakness is not inherent to the theories but to the frameworks in which they're defined: machine models which thread the heap through evaluation. Since these frameworks allocate each abstract resource in the heap, the constituent theories of environment analysis conflate co-live resources identified in the abstract, such as recursively-created bindings. We present heap fragments as a general technique to allow these theories to reason about recursion in a general and robust way. We instantiate abstract counting in a heap-fragment framework and compare its performance to a precursor entire-heap framework. We also sketch an approach to realizing binding invariants, a more powerful environment analysis, in the heap-fragment framework.

Google v. Oracle is a case involving the meaning of a copyright in computer software. The trial determined that Google copied many thousands of lines of code that had been written by Oracle. The code that was taken defined the existence of specific computing functions, determining which of two number is the larger one, as an example. Although Google did take these definitions, its programmers re-wrote the code that was needed to perform the function. Once taken, the code was used by Google to create (and then sell) the Android system for cell phones.The first major issue in the case is understanding what owning a copyright in computer software means. All agree that a copyright only protects an “expression” and does not protect any underlying ideas. The first dispute is whether the defining code is an expression or an idea. The second issue in the case is the meaning of the “fair use” defense where copying is allowed even though the copyright exists. Here, the main question is whether allowing computer programs to be written in a way that favors easy interoperability constitutes fair use.The brief submitted by the team of researchers based at U.Mass. Dartmouth and U.Mass. Lowell and written by Professor Clifford of the U.Mass. Law School only address the first issue. It argues that the declaring code that was taken is clearly expressive based on the Team’s research findings that there is significant variation of expression shown in all computer programs, even the most basic.

The purpose of this section is to establish that demand 0CFA is sound w.r.t. an exact forward semantics. To do so, we will establish that demand 0CFA is sound w.r.t. an exact demand semantics and that this demand semantics has a formal correspondence to an exact forward semantics. We term the exact demand semantics we define demand evaluation. To a first approximation, demand evaluation computes a subderivation of a full derivation of a program’s evaluation, where the particular subderivation computed is determined in part by the program subexpression. This is only an approximate description of the action of demand evaluation for a few reasons: first, one may successfully apply demand evaluation to unreachable program subexpressions, computing derivations that don’t appear in the derivation of the whole program’s evaluation; second, the product of demand evaluation isn’t necessarily a single contiguous subderivation but may instead be a set of related subderivations obtained (conceptually) by removing irrelevant judgments from a larger derivation. Although our intuition is rooted in derivations, we formalize demand evaluation as exact demand analyses related to program configurations, analogous to how we formalized demand 0CFA as approximate demand analyses related to program expressions. Doing so decreases the conceptual distance between demand 0CFA and demand evaluation, making soundness easier to establish. In order to connect demand evaluation to forward evaluation, we reify derivations from exact demand analyses and formally establish a correspondence between those derivations and forward derivations in a technical report [1].

This special issue represents a selection of the best papers of TFP'13 and TFP'14, in substantially revised versions.The authors of the three best papers in each instance were invited to submit revised versions of their research, reflecting new developments since the TFP version of the paper.In each case, at least 30% of the material in the journal paper is new.The Symposium on Trends in Functional Programming (TFP) is dedicated to promoting new research directions related to the field of functional programming and to investigate the relationships of functional programming with other branches of computer science.It is designed to be a platform for novel and upcoming research, offering a lively environment for presenting the latest research results.A formal post-symposium refereeing process then selects a high-quality set of articles from those presented at the symposium and submitted for formal publication.The journal versions of the best papers from these proceedings then offer an opportunity for the authors to take a longer term view of their research effort s and to present new results since the original presentation at TFP.This special issue covers two instances of the TFP symposium.TFP 2013 was held in Provo, Utah in the United States of America in May 2013, hosted by Brigham Young University.For TFP 2013, 24 papers were submitted to the formal refereeing process and 10 of these were accepted by the programme committee.TFP 2014 was the main event of a series of events around functional programming, was held in Soesterberg, the Netherlands in May 2014.In total, 22 papers were submitted to the formal refereeing process and eight papers were accepted.TFP traditionally pays special attention to research students, acknowledging that students are almost by definition part of new subject trends.These papers also receive an extra round of feedback by the programme committee before they are submitted to the standard review process for formal publication.In this way, students can improve their papers before they compete within a full formal refereeing process.This is often a useful stepping stone in the process of academic publications, although in this specific special issue no student papers are presented.Details on TFP can be found on this webpage: http: //www.tifp.org/ .The paper by Joachim Breitner, Call Arity, discusses an analysis to improve run-time performance of functional programs, by eta-expanding functions based on how they are used.Introducing the notion of co-call graphs, it improves on existing analyses, enabling fusion for foldl-like functions.It has been implemented in the de facto standard Haskell compiler GHC, and part of the default setting since version 7.10.1.The paper shows by means of a benchmark that the gains are large in some cases, and good overall.Debugging has always been a challenge for (lazy) functional languages.In the paper by Maarten Faddegon and Olaf Chitil, the authors apply generic programming techniques to reduce to burden on the programmer for defining how values observed, and use metaprogramming techniques to specify which parts of those values can be observed.We would like to thank the sponsors for these two TFP instances: Erlang Solutions Ltd, Well-

As the software industry enters the era of language-oriented programming, it needs programmable programming languages.

Data-race detection is the problem of determining if a concurrent program has a data-race in some execution and input; it has been long studied and often solved. The research in this paper reprises the problem in the context of task parallel programs with the intent to prove, via model checking, the absence of data-race on any feasible schedule for a given input. Many of the correctness properties afforded by task parallel programming models such as OpenMP, Cilk, X10, Chapel, Habanero, etc. rely on data-race freedom. Model checking for data-race, presented here, is in contrast to recent work using run-time monitoring, log analysis, or static analysis which are complete or sound but never both. The model checking algorithm builds a happens-before relation from the program execution and uses that relation to detect data-race similar to many solutions that reason over a single observed execution. Unlike those solutions, model checking generates additional program schedules sufficient to prove data-race freedom over all schedules on the given input. The approach is evaluated in a Java implementation of Habanero using the JavaPathfinder model checker. The results, when compared to existing data-race detectors in Java Pathfinder, show a significant reduction in the time required for proving data race freedom.

Abstract Enumerations represented as bijections between the natural numbers and elements of some given type have recently garnered interest in property-based testing because of their efficiency and flexibility. There are, however, many ways of defining these bijections, some of which are better than others. This paper offers a new property of enumeration combinators called fairness that identifies enumeration combinators that are better suited to property-based testing. Intuitively, the result of a fair combinator indexes into its argument enumerations equally when constructing its result. For example, extracting the nth element from our enumeration of three-tuples indexes about $\sqrt[3]{n}$ elements into each of its components instead of, say, indexing $\sqrt[2]{n}$ into one and $\sqrt[4]{n}$ into the other two, as you would if a three-tuple were built out of nested pairs. Similarly, extracting the nth element from our enumeration of a three-way union returns an element that is $\frac{n}{3}$ into one of the argument enumerators. The paper presents a semantics of enumeration combinators, a theory of fairness, proofs establishing fairness of our new combinators and that some combinations of fair combinators are not fair. We also report on an evaluation of fairness for the purpose of finding bugs in programming-language models. We show that fair enumeration combinators have complementary strengths to an existing, well-tuned ad hoc random generator (better on short time scales and worse on long time scales) and that using unfair combinators is worse across the board.

Exploring Computer Science (ECS) is a high school introductory computer science class designed to increase student interest in CS. Utah is the first state to offer ECS statewide and use it to meet a high school graduation requirement. Over the past four years, 150 teachers have been trained as Utah ECS teachers and over 10,000 Utah students have taken the class. The Utah initiative is unique because it is the first to deploy ECS in a non-urban environment and with a modified half-year curriculum that includes no additional equipment costs. This paper discusses how the Utah deployment was organized, reports its results and unique difficulties, and offers lessons for deployments with similar characteristics: statewide, rural, and limited resources.

Bithoven is a prolific composer of approximately 1.079363 * 10^239 different compositions based on four-part harmony and basic chord progressions. It is combined with a purely functional audio synthe- sis engine based on the Ricoh RP2A03, found in the 1985 Nintendo Entertainment System (NES). The synthesis engine is parameter- ized over a band of instruments and styles of play, so each com- position can be played in one of approximately 4.22234 * 10^41 different arrangements or "NEStrations".

This paper presents a Coq library that lifts an abstract yet precise notion of running-time into the type of a function. Our library is based on a monad that counts abstract steps, controlled by one of the monadic operations. The monad’s computational content, however, is simply that of the identity monad so programs written in our monad (that recur on the natural structure of their arguments) extract into idiomatic OCaml code. We evaluated the expressiveness of the library by proving that red-black tree insertion and search, merge sort, insertion sort, Fibonacci, iterated list insertion, BigNum addition, and Okasaki’s Braun Tree algorithms all have their expected running times.

Many probabilistic programming languages allow programs to be run under constraints in order to carry out Bayesian inference. Running programs under constraints could enable other uses such as rare event simulation and probabilistic verification—except that all such probabilistic languages are necessarily limited because they are defined or implemented in terms of an impoverished theory of probability. Measure-theoretic probability provides a more general foundation, but its generality makes finding computational content difficult. We develop a measure-theoretic semantics for a first-order probabilistic language with recursion, which interprets programs as functions that compute preimages. Preimage functions are generally uncomputable, so we derive an abstract semantics. We implement the abstract semantics and use the implementation to carry out Bayesian inference, stochastic ray tracing (a rare event simulation), and probabilistic verification of floating-point error bounds.

The creation of a programming language calls for guiding principles that point the developers to goals. This article spells out the three basic principles behind the 20-year development of Racket. First, programming is about stating and solving problems, and this activity normally takes place in a context with its own language of discourse; good programmers ought to formulate this language as a programming language. Hence, Racket is a programming language for creating new programming languages. Second, by following this language-oriented approach to programming, systems become multi-lingual collections of interconnected components. Each language and component must be able to protect its specific invariants. In support, Racket offers protection mechanisms to implement a full language spectrum, from C-level bit manipulation to soundly typed extensions. Third, because Racket considers programming as problem solving in the correct language, Racket also turns extra-linguistic mechanisms into linguistic constructs, especially mechanisms for managing resources and projects. The paper explains these principles and how Racket lives up to them, presents the evaluation framework behind the design process, and concludes with a sketch of Racket's imperfections and opportunities for future improvements.

With the right tools, floating-point code can be debugged like any other code, drastically improving its accuracy and reliability.

Due to the varying latencies between memory banks, efficient shared memory access is challenging on modern NUMA architectures. This has a major impact on the shared memory performance of parallel programs, particularly those written in languages with automatic memory management. This paper presents a performance evaluation of distributed and shared heap implementations of parallel Haskell on a state-of-the-art physical shared memory NUMA machine. The evaluation exposes bottlenecks in the shared-memory management, which results in limits to scalability beyond 25 out of the 48 cores. We demonstrate that a hybrid system, GUMSMP, that combines both distributed and shared heap abstractions consistently outperforms the shared memory GHC implementation on seven benchmarks by a factor of 3.3 on average. Specifically, we show that the best results are obtained when sharing memory only within a single NUMA region, and using distributed memory system abstractions across the regions.

Asynchronous message passing is an important paradigm in writing applications for embedded heterogeneous multicore systems. The Multicore Association (MCA), an industry consortium promoting multicore technology, is working to standardize message passing into a single API, MCAPI, for bare metal implementation and portability across platforms. Correctness in such an API is difficult to reason about manually, and testing against reference solutions is equally difficult as reference solutions implement an unknown set of allowed behaviors, and programmers have no way to directly control API internals to expose or reproduce errors. This paper provides a way to encode an MCAPI execution as a Satisfiability Modulo Theories (SMT) problem, which if satisfiable, yields a feasible execution schedule on the same trace, such that it resolves non-determinism in the MCAPI runtime in a way that it now fails user provided assertions. The paper proves the problem is NP-complete. The encoding is useful for test, debug, and verification of MCAPI program execution. The novelty in the encoding is the direct use of match pairs (potential send and receive couplings). Match-pair encoding for MCAPI executions, when compared to other encoding strategies, is simpler to reason about, results in significantly fewer terms in the SMT problem, and captures feasible behaviors that are ignored in previously published techniques. Further, to our knowledge, this is the first SMT encoding that is able to run in infinite-buffer semantics, meaning the runtime has unlimited internal buffering as opposed to no internal buffering. Results demonstrate that the SMT encoding, restricted to zero-buffer semantics, uses fewer clauses when compared to another zero-buffer technique, and it runs faster and uses less memory. As a result the encoding scales well for programs with high levels of non-determinism in how sends and receives may potentially match.

Methods for mathematically basic and precise description of system behavior at discrete interfaces have been developed by David Parnas and his groups and collaborators over many years. Total functions can play a crucial role as constructive and effectively executable semantics for various levels of these descriptions. Straightforward analysis and transformation techniques for functional programs, particularly effective for total functions, can be used as significant steps towards automated generation of implementations. Theoretical claims are supported by practical examples. The focus is on insight into applications from the functional perspective rather than on innovations in functional programming itself.

Given the widespread use of memory-safe languages, students must understand garbage collection well. Following a constructivist philosophy, an effective approach would be to have them implement garbage collectors. Unfortunately, a full implementation depends on substantial knowledge of compilers and runtime systems, which many courses do not cover or cannot assume. This paper presents an instructive approach to teaching GC, where students implement it atop a simplified stack and heap. Our approach eliminates enormous curricular dependencies while preserving the essence of GC algorithms. We take pains to enable testability, comprehensibility, and facilitates debugging. Our approach has been successfully classroom-tested for several years at several institutions.

Continuation marks are a programming language feature which generalizes stack inspection. Despite its usefulness, this feature has not been adopted by languages which rely on stack inspection, e.g., for dynamic security checks. One reason for this neglect may be that continuation marks do not yet enjoy a transformation to the plain λ-calculus which would allow higher-order languages to provide continuation marks at little cost. We present a transformation from the call-by-value λ-calculus augmented with continuation marks to the pure call-by-value λ-calculus. We discuss how such transformations simplify the construction of compilers which treat continuation marks correctly. We document how Redex, a domain-specific language for exploring language semantics, aided the discovery of correct transformations. We offer the sketch proof of a meaningpreservation theorem. Finally, we apply the transformation to JavaScript.

Asynchronous message passing is an important paradigm in writing applications for embedded heterogeneous multicore systems. The Multicore Association (MCA), an industry consortium promoting multicore technology, is working to standardize message passing into a single API, MCAPI, for bare metal implementation and portability across platforms. Correctness in such an API is difficult to reason about manually, and testing against reference solutions is equally difficult as reference solutions implement an unknown set of allowed behaviors, and programmers have no way to directly control API internals to expose or reproduce errors. This paper provides a way to encode an MCAPI execution as a Satisfiability Modulo Theories (SMT) problem, which if satisfiable, yields a feasible execution schedule on the same trace, such that it resolves non-determinism in the MCAPI runtime in a way that it now fails user provided assertions. The paper proves the problem is NP-complete. The encoding is useful for test, debug, and verification of MCAPI program execution. The novelty in the encoding is the direct use of match pairs (potential send and receive couplings). Match-pair encoding for MCAPI executions, when compared to other encoding strategies, is simpler to reason about, results in significantly fewer terms in the SMT problem, and captures feasible behaviors that are ignored in previously published techniques. Further, to our knowledge, this is the first SMT encoding that is able to run in infinite-buffer semantics, meaning the runtime has unlimited internal buffering as opposed to no internal buffering. Results demonstrate that the SMT encoding, restricted to zero-buffer semantics, uses fewer clauses when compared to another zero-buffer technique, and it runs faster and uses less memory. As a result the encoding scales well for programs with high levels of non-determinism in how sends and receives may potentially match.