7,482 papers · page 168 of 375
The notion of context in functional languages no longer refers just to variables in scope. Context can capture additional properties of variables (usage patterns in linear logics; caching requirements in dataflow languages) as well as additional resources or properties of the exe…
Type inference - the problem of determining whether a program is well-typed - is well-understood. In contrast, elaboration - the task of constructing an explicitly-typed representation of the program - seems to have received relatively little attention, even though, in a non-loca…
This paper presents a personal, qualitative case study of a first course using How to Design Programs and its functional teaching languages. The paper reconceptualizes the book's six-step design process as an eight-step design process ending in a new "review and refactor" step. I…
In a Software-Defined Network (SDN), a central, computationally powerful controller manages a set of distributed, computationally simple switches. The controller computes a policy describing how each switch should route packets and populates packet-processing tables on each switc…
The root cause for confidentiality and integrity attacks against computing systems is insecure information flow. The complexity of modern systems poses a major challenge to secure end-to-end information flow, ensuring that the insecurity of a single component does not render the …
Effect systems have the potential to help software developers, but their practical adoption has been very limited. We conjecture that this limited adoption is due in part to the difficulty of transitioning from a system where effects are implicit and unrestricted to a system with…
Current languages for safely manipulating values with names only support term languages with simple binding syntax. As a result, no tools exist to safely manipulate code written in those languages for which name problems are the most challenging. We address this problem with Rome…
SMT-based checking of refinement types for call-by-value languages is a well-studied subject. Unfortunately, the classical translation of refinement types to verification conditions is unsound under lazy evaluation. When checking an expression, such systems implicitly assume that…
Is Haskell a dependently typed programming language? Should it be? GHC's many type-system features, such as Generalized Algebraic Datatypes (GADTs), datatype promotion, multiparameter type classes, and type families, give programmers the ability to encode domain-specific invarian…
Functional Reactive Programming (FRP) provides a method for programming continuous, reactive systems by utilizing signal functions that, abstractly, transform continuous input signals into continuous output signals. These signals may also be streams of events, and indeed, by allo…
The HipHop Virtual Machine (HHVM) is a JIT compiler and runtime for PHP. While PHP values are dynamically typed, real programs often have latent types that are useful for optimization once discovered. Some types can be proven through static analysis, but limitations in the ahead-…
Gradual typing combines static and dynamic typing flexibly and safely in a single programming language. To do so, gradually typed languages implicitly insert casts where needed, to ensure at runtime that typing assumptions are not violated by untyped code. However, the implicit n…
Wildcard annotations can improve the generality of Java generic libraries, but require heavy manual effort. We present an algorithm for refactoring and inferring more general type instantiations of Java generics using wildcards. Compared to past approaches, our work is practical …
A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, Scala unifies concepts from object and module systems. An essential ingredient of this unification is the concept of objects with type members, which ca…
Static analysis for JavaScript can potentially help programmers find errors early during development. Although much progress has been made on analysis techniques, a major obstacle is the prevalence of libraries, in particular jQuery, which apply programming patterns that have det…
Testing and static analysis can help root out bugs in programs, but not in data. This paper introduces data debugging, an approach that combines program analysis and statistical analysis to automatically find potential data errors. Since it is impossible to know a priori whether …
Developers who set a breakpoint a few statements too late or who are trying to diagnose a subtle bug from a single core dump often wish for a time-traveling debugger. The ability to rewind time to see the exact sequence of statements and program values leading to an error has gre…
We introduce RATE TYPES, a novel type system to reason about and optimize data-intensive programs. Built around stream languages, RATE TYPES performs static quantitative reasoning about stream rates -- the frequency of data items in a stream being consumed, processed, and produce…
Dynamic taint analysis is a well-known information flow analysis problem with many possible applications. Taint tracking allows for analysis of application data flow by assigning labels to data, and then propagating those labels through data flow. Taint tracking systems tradition…
We describe an algorithm to perform symbolic execution of a multithreaded program starting from an arbitrary program context. We argue that this can enable more efficient symbolic exploration of deep code paths in multithreaded programs by allowing the symbolic engine to jump dir…