When scripts in untyped languages grow into large programs, maintaining them becomes difficult. A lack of types in typical scripting languages means that programmers must (re)discover critical pieces of design information every time they wish to change ...

Higher-order abstract syntax (HOAS) is a simple, powerful technique for implementing object languages, since it directly supports common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. This is achieved by ...

Focusing is a proof-search strategy, originating in linear logic, that elegantly eliminates inessential nondeterminism, with one byproduct being a correspondence between focusing proofs and programs with explicit evaluation order. Higher-order abstract ...

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they ...

GADTs are at the cutting edge of functional programming and becomemore widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory of ...

This paper introduces a small but useful generalisation to the 'derivative' operation on datatypes underlying Huet's notion of 'zipper', giving a concrete representation to one-hole contexts in data which is undergoing transformation. This operator, '...

Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-centred programming, session types have been studied over the last decade for a wide range of process calculi and ...

The C language definition leaves the sizes and layouts of types partially unspecified. When a C program makes assumptions about type layout, its semantics is defined only on platforms (C compilers and the underlying hardware) on which those assumptions ...

This paper takes a fresh look at the problem of precise verification of heap-manipulating programs using first-order Satisfiability-Modulo-Theories (SMT) solvers. We augment the specification logic of such solvers by introducing the Logic of Interpreted ...

Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis ...

This paper presents a generalization of standard effect systems that we call contextual effects. A traditional effect system computes the effect of an expression e. Our system additionally computes the effects of the computational context in which e ...

This pearl develops a statement about parallel prefix computation in the spirit of Knuth's 0-1-Principle for oblivious sorting algorithms. It turns out that 0-1 is not quite enough here. The perfect hammer for the nails we are going to drive in is ...

Machine-checked proofs of properties of programming languages have become acritical need, both for increased confidence in large and complex designsand as a foundation for technologies such as proof-carrying code. However, constructing these proofs ...

Jane Street Capital is a successful proprietary trading company that has shifted from developing software in mainstream programming languages to developing software almost entirely in OCaml, a statically typed functional programming language that has ...

An ad hoc data source is any semistructured data source for which useful data analysis and transformation tools are not readily available. Such data must be queried, transformed and displayed by systems administrators, computational biologists, ...

A lens is a bidirectional program. When read from left toright, it denotes an ordinary function that maps inputs to outputs. When read from right to left, it denotes an ''update translator'' that takes an input together with an updated output and ...

The subtyping test consists of checking whether a type t is a descendant of a type r (Agrawal et al. 1989). We study how to perform such a test efficiently, assuming a dynamic hierarchy when new types are inserted at run-time. The goal is to achieve ...

Self-adjusting computation enables writing programs that can automatically and efficiently respond to changes to their data (e.g., inputs). The idea behind the approach is to store all data that can change over time in modifiable references and to let ...

Shape analyses are concerned with precise abstractions of the heap to capture detailed structural properties. To do so, they need to build and decompose summaries of disjoint memory regions. Unfortunately, many data structure invariants require ...

We describe a general technique for building abstract interpreters over powerful universally quantified abstract domains that leverage existing quantifier-free domains. Our quantified abstract domain can represent universally quantified facts like ∀i(0 ≤...