26,098 papers · page 450 of 1,305
Abstract We present a model of computation that heavily emphasizes the concept of duality and the interaction between opposites–production interacts with consumption. The symmetry of this framework naturally explains more complicated features of programming languages through rela…
Abstract In higher order settings, control-flow analysis aims to model the propagation of both data and control by finitely approximating program behaviors across all possible executions. The polyvariance of an analysis describes the number of distinct abstract representations, o…
Abstract The most successful systems for “big data” processing have all adopted functional APIs. We present a new programming model, we call function passing , designed to provide a more principled substrate, or middleware, upon which to build data-centric distributed systems lik…
We consider the task of constructing 2-3 trees. Given a sequence of elements we seek to build a 2-3 tree–in linear time–that contains the elements in symmetric order. We discuss three approaches: top-down, bottom-up, and incremental. The incremental approach is more flexible than…
Comparison networks offer an attractive framework for studying parallel sorting algorithms. The visual presentation of such hard-wired networks makes processes easy to conceptualize without the overhead of programming syntax or the semantic complications of concurrency. Though si…
Batcher’s “merge exchange” sorting network, discussed in a previous pearl (Hinze & Martin, 2016), remains one of the best practical algorithms for oblivious sorting, even almost half a century after its inception. So it is surprising that an algorithm with exactly the same level …
Many students complete PhDs in functional programming each year. As a service to the community, the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year.
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundatio…
Functional languages are uniquely suited to providing programmers with a programming model for parallel and concurrent computing. This is reflected in the wide range of work that is currently underway, both on parallel and concurrent functional languages, as well as on bringing f…
Abstract A bidirectional transformation is a pair of mappings between source and view data objects, one in each direction. When the view is modified, the source is updated accordingly with respect to some laws. One way to reduce the development and maintenance effort of bidirecti…
Abstract A Computer Science introduction course ought to focus on exciting students about the subject matter and on problem solving through the methodical design of programs. An effective way to achieve both is through the development of functional video games. As most students a…
Abstract ML is two languages in one: there is the core , with types and expressions, and there are modules , with signatures, structures, and functors. Modules form a separate, higher-order functional language on top of the core. There are both practical and technical reasons for…
Abstract Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an ill-typed program goes wrong. First, given an ill-typed…
Abstract Database query engines use pull-based or push-based approaches to avoid the materialization of data across query operators. In this paper, we study these two types of query engines in depth and present the limitations and advantages of each engine. Similarly, the program…
Abstract Contract systems have come to play a vital role in many aspects of software engineering. This has resulted in a wide variety of approaches to enforcing contracts—ranging from the straightforward pre-condition and post-condition checking of Eiffel to lazy, optional, and p…
Abstract Generalized Algebraic Data Types, or simply GADTs, can encode non-trivial properties in the types of the constructors. Once such properties are encoded in a datatype, however, all code manipulating that datatype must provide proof that it maintains these properties in or…
For specifying and reasoning about object-based programs, it is often attractive for contracts to be expressed using calls to pure methods. It is useful for pure methods to have contracts, including read effects, to support local reasoning based on frame conditions. This leads to…
In this article, we consider the termination problem of probabilistic programs with real-valued variables. The questions concerned are: qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected terminat…
We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natu…
Non-termination is the root cause of a variety of program bugs, such as hanging programs and denial-of-service vulnerabilities. This makes an automated analysis that can prove the absence of such bugs highly desirable. To scale termination checks to large systems, an interprocedu…