7,482 papers · page 129 of 375
Gradual typing allows programs to enjoy the benefits of both static typing and dynamic typing. While it is often desirable to migrate a program from more dynamically-typed to more statically-typed or vice versa, gradual typing itself does not provide a way to facilitate this migr…
Gradual typing allows programmers to use both static and dynamic typing in a single program. However, a well-known problem with sound gradual typing is that the interactions between static and dynamic code can cause significant performance degradation. These performance pitfalls …
Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.) solves this by considering only truncated types, roughly corr…
We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the n…
When designing a type system, we may want to mechanically check the design to guide its further development. We describe algorithms that perform symbolic reasoning about executable models of type systems. The algorithms support three queries. First, they check type soundness and …
We present lambda_sym, a typed λ-calculus for lenient symbolic execution , where some language constructs do not recognize symbolic values. Its type system, however, ensures safe behavior of all symbolic values in a program. Our calculus extends a base occurrence typing system wi…
A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graph where the edges are labeled with different types of opening and closing parentheses, and the reachability information is computed via paths whose parentheses are properly …
The theory of strings with concatenation has been widely argued as the basis of constraint solving for verifying string-manipulating programs. However, this theory is far from adequate for expressing many string constraints that are also needed in practice; for example, the use o…
This paper shows how to build a sparse tensor algebra compiler that is agnostic to tensor formats (data layouts). We develop an interface that describes formats in terms of their capabilities and properties, and show how to build a modular code generator where new formats can be …
Higher-order recursion schemes (HORS) have recently emerged as a promising foundation for higher-order program verification. We examine the impact of enriching HORS with linear types. To that end, we introduce two frameworks that blend non-linear and linear types: a variant of th…
In a dependently typed language, we can guarantee correctness of our programs by providing formal proofs. To check them, the typechecker elaborates these programs and proofs into a low level core language. However, this core language is by nature hard to understand by mere humans…
Memory-management support for lock-free data structures is well known to be a tough problem. Recent work has successfully reduced the overhead of such schemes. However, applying memory-management support to a data structure remains complex and, in many cases, requires redesigning…
New non-volatile memory (NVM) technologies enable direct, durable storage of data in an application's heap. Durable, randomly accessible memory facilitates the construction of applications that do not lose data at system shutdown or power failure. Existing NVM programming framewo…
Dependent types are a powerful tool for maintaining program invariants. To take advantage of this aspect in real-world programming, efforts have been put into enriching dependently typed languages with missing constructs, most notably, effects. This paper presents a language that…
Dynamic programming languages such as Python and Ruby are widely used, and much effort is spent on making them efficient. One substantial research effort in this direction is the enabling of parallel code execution. While there has been significant progress, making dynamic collec…
Up-to techniques are used to make it easier—or feasible—to construct, for instance, proofs of bisimilarity. This text shows how many up-to techniques can be framed as size-preserving functions , using sized types to keep track of sizes. Through a number of examples it is argued t…
We study the problem of parametric parallel complexity analysis of concurrent, message-passing programs. To make the analysis local and compositional, it is based on a conservative extension of binary session types, which structure the type and direction of communication between …
Embedding a modern language runtime as a component in a larger software system is popular these days. Communication between these systems often requires keeping references to each others' objects. In this paper we present and discuss the problem of cross-component memory manageme…
A real-world distributed system is rarely implemented as a standalone monolithic system. Instead, it is composed of multiple independent interacting components that together ensure the desired system-level specification. One can scale systematic testing to large, industrial-scale…
There has long been speculation in the scientific literature on how to dynamically enforce parametricity such as that yielded by System F. Almost 20 years ago, Sumii and Pierce proposed a formal compiler from System F into the cryptographic lambda calculus: an untyped lambda calc…