7,482 papers · page 197 of 375
Integrating a database query language into a programming language is becoming increasingly important in recently emerging high-level cloud computing and other applications, where efficient and sophisticated data manipulation is required during computation. This paper reports on s…
We characterize the data type of terms with bindings, freshness and substitution, as an initial model in a suitable Horn theory. This characterization yields a convenient recursive definition principle, which we have formalized in Isabelle/HOL and employed in a series of case stu…
De Bruijn indices are a well known technique for programming with names and binders. They provide a representation that is both simple and canonical.
We make monadic components more reusable and robust to changes by employing two new techniques for virtualizing the monad stack: the monad zipper and monad views. The monad zipper is a higher-order monad transformer that creates virtual monad stacks by ignoring particular layers …
We present a technique, based on the use of first-class control operators, enabling programs to maintain and invoke rollback logs for sequences of reversible effects. Our technique is modular, in that it provides complete separation between some library of effectful operations, a…
Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effe…
Many useful programming constructions can be expressed as monads. Examples include probabilistic modeling, functional reactive programming, parsing, and information flow tracking, not to mention effectful functionality like state and I/O. In this paper, we present a type-based re…
Agda is a modern functional programming language equipped with an interactive proof assistant as its developing environment. Its features include dependent types, type universe, inductive and coinductive families of types, pattern matching, records, and nested parameterized modul…
We present a Kripke logical relation for showing the correctness of program transformations based on a type-and-effect system for an ML-like programming language with higher-order store and dynamic allocation.
Motivated by developing a memory management system that allows functional languages to seamlessly inter-operate with C, we propose an efficient non-moving garbage collection algorithm based on bitmap marking and report its implementation and performance evaluation.
Pushdown models are better than control-flow graphs for higher-order flow analysis. They faithfully model the call/return structure of a program, which results in fewer spurious flows and increased precision. However, pushdown models require that calls and returns in the analyzed…
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. The key to handling large data objects that are subject to relatively small modifications is to process …
Implementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that manipulate syntax know that dealing with name binding is difficult to do well. Operations such as α-equivalence and capture-avoiding substitution seem simple, yet subtle bugs o…
A classic problem in parallel computing is determining whether to execute a task in parallel or sequentially. If small tasks are executed in parallel, the task-creation overheads can be overwhelming. If large tasks are executed sequentially, processors may spin idle. This granula…
The flexibility of dynamically typed languages such as JavaScript, Python, Ruby, and Scheme comes at the cost of run-time type checks. Some of these checks can be eliminated via control-flow analysis. However, traditional control-flow analysis (CFA) is not ideal for this task as …
Assertions are a familiar and widely used bug detection technique. Traditional assertion checking, however, is performed synchronously, imposing its full cost on the runtime of the program. As a result, many useful kinds of checks, such as data structure invariants and heap analy…
In previous work, we presented rules for defining overloaded functions that ensure type safety under symmetric multiple dispatch in an object-oriented language with multiple inheritance, and we showed how to check these rules without requiring the entire type hierarchy to be know…
In this paper we introduce a new method for pessimistically implementing composable, nestable atomic statements. Our mechanism, called shelters, is inspired by the synchronization strategy used in the Jade programming language. Unlike previous lock-based pessimistic approaches, o…
This paper focuses on extensibility, the ability of a programmer using a particular language to extend the expressiveness of that language. This paper explores how to provide an interesting notion of extensibility by virtualizing the interface between code and data. A virtual val…
Parallel or incremental versions of an algorithm can significantly outperform their counterparts, but are often difficult to develop. Programming models that provide appropriate abstractions to decompose data and tasks can simplify parallelization. We show in this work that the s…