Standard object out: streaming objects with polymorphic write streams
We propose standard object out, an object-oriented analog to the output part of the Unix standard input output library.
26,098 papers · page 370 of 1,305
Minimal Session Types (Pearl)
Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the pi-calculus and for languages such as Java. A session type specifies what and when should be exchanged through a channel. Central to sessio…
Eventually Sound Points-To Analysis with Specifications
Static analyses make the increasingly tenuous assumption that all source code is available for analysis; for example, large libraries often call into native code that cannot be analyzed. We propose a points-to analysis that initially makes optimistic assumptions about missing cod…
Julia's Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl)
The Julia programming language supports multiple dispatch and provides a rich type annotation language to specify method applicability. When multiple methods are applicable for a given call, Julia relies on subtyping between method signatures to pick the correct method to invoke.…
How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4
The P4 programming language offers high-level, declarative abstractions that bring the flexibility of software to the domain of networking. Unfortunately, the main abstraction used to represent packet data in P4, namely header types, lacks basic safety guarantees. Over the last f…
Garbage-Free Abstract Interpretation Through Abstract Reference Counting
Abstract garbage collection is the application of garbage collection to an abstract interpreter. Existing work has shown that abstract garbage collection can improve both the interpreter’s precision and performance. Current approaches rely on heuristics to decide when to apply ab…
Godot: All the Benefits of Implicit and Explicit Futures
Concurrent programs often make use of futures, handles to the results of asynchronous operations. Futures provide means to communicate not yet computed results, and simplify the implementation of operations that synchronise on the result of such asynchronous operations. Futures c…
Deep Static Modeling of invokedynamic
Java 7 introduced programmable dynamic linking in the form of the invokedynamic framework. Static analysis of code containing programmable dynamic linking has often been cited as a significant source of unsoundness in the analysis of Java programs. For example, Java lambdas, intr…
Fling - A Fluent API Generator
We present the first general and practical solution of the fluent API problem - an algorithm, that given a deterministic language (equivalently, LR(k), k >= 0 language) encodes it in an unbounded parametric polymorphism type system employing only a polynomial number of types. The…
Transferring Obligations Through Synchronizations
One common approach for verifying safety properties of multithreaded programs is assigning appropriate permissions, such as ownership of a heap location, and obligations, such as an obligation to send a message on a channel, to each thread and making sure that each thread only pe…
Semantic Patches for Java Program Transformation (Experience Report)
Developing software often requires code changes that are widespread and applied to multiple locations. There are tools for Java that allow developers to specify patterns for program matching and source-to-source transformation. However, to our knowledge, none allows for transform…
Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Brave New Idea Paper)
Many of today’s software systems are parallel or concurrent. With the rise of Node.js and more generally event-loop architectures, many systems need to handle concurrency. However, its non-deterministic behavior makes it hard to reproduce bugs. Today’s interactive debuggers unfor…
MagpieBridge: A General Approach to Integrating Static Analyses into IDEs and Editors (Tool Insights Paper)
In the past, many static analyses have been created in academia, but only a few of them have found widespread use in industry. Those analyses which are adopted by developers usually have IDE support in the form of plugins, without which developers have no convenient mechanism to …
Motion Session Types for Robotic Interactions (Brave New Idea Paper)
Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world. Today, these applications are typically programmed in low-level imperative programming lan…
NumLin: Linear Types for Linear Algebra
We present NumLin, a functional programming language whose type system is designed to enforce the safe usage of the APIs of low-level linear algebra libraries (such as BLAS/LAPACK). We do so through a brief description of its key features and several illustrative examples. We sho…
Lifestate: Event-Driven Protocols and Callback Control Flow
Developing interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine th…
On Satisfiability of Nominal Subtyping with Variance
Nominal type systems with variance, the core of the subtyping relation in object-oriented programming languages like Java, C# and Scala, have been extensively studied by Kennedy and Pierce: they have shown the undecidability of the subtyping between ground types and proposed the …
A Typing Discipline for Hardware Interfaces
Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) Cores with the communication between these IP Cores being governed by well described interaction protocols. However, there is a disconnect between the machine readable specification of the…
Reliable State Machines: A Framework for Programming Reliable Cloud Services
Building reliable applications for the cloud is challenging because of unpredictable failures during a program’s execution. This paper presents a programming framework, called Reliable State Machines (RSMs), that offers fault-tolerance by construction. In our framework, an applic…
Towards Language-Parametric Semantic Editor Services Based on Declarative Type System Specifications (Brave New Idea Paper)
Editor services assist programmers to more effectively write and comprehend code. Implementing editor services correctly is not trivial. This paper focuses on the specification of semantic editor services, those that use the semantic model of a program. The specification of refac…