7,482 papers · page 271 of 375
Exploiting spatial and temporal locality is essential for obtaining high performance on modern computers. Writing programs that exhibit high locality of reference is difficult and error-prone. Compiler researchers have developed loop transformations that allow the conversion of p…
The "size-change termination" principle for a first-order functional language with well-founded data is: a program terminates on all inputs if every infinite call sequence (following program control flow) would cause an infinite descent in some data values.Size-change analysis is…
No abstract available.
This invited talk will give a personal view of the field of computer security and summarize some ways that methods from the study of programming language principles can be applied to problems in computer security. Some background information is provided here in this short documen…
We introduce a new method, combination of random testing and abstract interpretation, for the analysis of programs featuring both probabilistic and non-probabilistic nondeterminism. After introducing "ordinary" testing, we show how to combine testing and abstract interpretation a…
We present a variant of Proof-Carrying Code (PCC) in which the trusted inference rules are represented as a higherorder logic program, the proof checker is replaced by a nondeterministic higher-order logic interpreter and the proof by an oracle implemented as a stream of bits tha…
We present a type system for a language based on $F_\\leq$ , which allows certain type annotations to be elided in actual programs. Local type inference determines types by a combination of type propagation and local constraint solving, rather than by global constraint solving. W…
We present a novel approach to scalable implementation of type-based flow analysis with polymorphic subtyping. Using a new presentation of polymorphic subytping with instantiation constraints, we are able to apply context-free language (CFL) reachability techniques to type-based …
The ambient logic has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. To understand the extensionality and the intensionality of the logic, the equivalence on MA proces…
In a wide-area distributed system it is often impractical to synchronise software updates, so one must deal with many coexisting versions. We study static typing support for modular wide-area programming, modelling separate compilation/linking and execution of programs that inter…
Record calculi use labels to distinguish between the elements of products and sums. This paper presents a novel variation, type-indexed rows, in which labels are discarded and elements are indexed by their type alone. The calculus, λTIR, can express tuples, recursive datatypes, m…
This paper addresses the design and verification of infrastructure for mobile computation. In particular, we study language primitives for communication between mobile agents. They can be classi ed into two groups. At a low level there are location dependent primitives that requi…
We presen t an object-oriented calculus whic hallows arbitrary hiding of methods in protot ypes, even in the presence of binary methods and friend functions. This combination of features permits complete control of the in terface a class exposes to the remainder of a program (whi…
By combining existing type systems with standard type-based compilation techniques, we describe how to write strongly typed programs that include a function that acts as a t racing garbage collector for the program. Since the garbage collector is an explicit function, we do not n…
We provide a parametric framework for verifying safety properties of concurrent Java programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to error-detection algorithms that are more precise than existing technique…
We present an operational semantics for parallel lazy evaluation that accurately models the parallel behaviour of the non-strict parallel functional language GpH. Parallelism is modelled synchronously, that is, single reductions are carried out separately then combined before pro…
This paper generalises the flattening transformation - a technique for the efficient implementation of nested data parallelism - and reconciles it with main stream functional programming. Nested data parallelism is significantly more expressive and convenient to use than the flat…
We describe an efficient technique for incorporating Baker's incremental garbage collection algorithm into the Spineless Tagless G-machine on stock hardware. This algorithm eliminates the stop/go execution associated with bulk copying collection algorithms, allowing the system to…
Quick Check is a tool which aids the Haskell programmer in formulating and testing properties of programs. Properties are described as Haskell functions, and can be automatically tested on random input, but it is also possible to define custom test data generators. We present a n…
I present a type-preserving translation that eliminates subtyping and bounded quantification without introducing any run-time costs. This translation is based on Mitchell and Pierce's encoding of bounded quantification using intersection types. I show that, previous negative obse…