The proofs of major results of Computability Theory like Rice, Rice-Shapiro or Kleene's fixed point theorem hide more information of what is usually expressed in their respec...
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 stor...
Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-centred programming, session types have...
This paper presents a demand-driven, flow-insensitive analysis algorithm for answering may-alias queries. We formulate the computation of alias queries as a CFL-reachability probl...
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 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 ...
Java programmers can document that the relationship between two objects is unchanging by declaring the field that encodes that relationship to be final. This information can be us...
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)disc...
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 a...
Kathleen Fisher, David Walker, Kenny Qili Zhu, Pet...
We propose a novel approach to proving the termination of heapmanipulating programs, which combines separation logic with cyclic proof within a Hoare-style proof system. Judgement...
James Brotherston, Richard Bornat, Cristiano Calca...