2,199 papers · page 76 of 110
The following theorem of Huet and Lévy forms the basis of all results on optimal reduction strategies for orthogonal term rewriting systems: every term not in normal form contains a needed redex, and repeated contraction of needed redexes results in the normal form, if the term u…
This paper describes proof-carrying code (PCC), a mechanism by which a host system can determine with certainty that it is safe to execute a program supplied (possibly in binary form) by an untrusted source. For this to be possible, the untrusted code producer must supply with th…
Defining the collecting semantics is usually the first crucial step in adapting the general methodology of abstract interpretation to the semantic framework or programming language at hand. In this paper we show how to define a collecting semantics for control flow analysis: due …
Pizza is a strict superset of Java that incorporates three ideas from the academic community: parametric polymorphism, higher-order functions, and algebraic data types. Pizza is defined by translation into Java and compiles into the Java Virtual Machine, requirements which strong…
We introduce the type theory λμv, a call-by-value variant of Parigot's λμ-calculus, as a Curry-Howard representation theory of classical propositional proofs. The associated rewrite system is Church-Rosser and strongly normalizing, and definitional equality of the type theory is …
In [Paige89], it was shown how to simulate a set machine in real-time on a RAM that provides cursor or even only pointer access to data. The underlying assumption was that the establishment of efficient data structures would be provided by some 'client' program. In the current pa…
The Asynchronous π-calculus, as recently proposed by Boudol and, independently, by Honda and Tokoro, is a subset of the π-calculus which contains no explicit operators for choice and output-prefixing. The communication mechanism of this calculus, however, is powerful enough to si…
Program specialization is a collection of program transformation techniques for improving program efficiency by exploiting some information available at compile-time about the input data. We show that current techniques for program specialization based on partial evaluation do no…
We investigate parametric polymorphism in message-based concurrent programming, focusing on behavioral equivalences in a typed process calculus analogous to the polymorphic lambda-calculus of Girard and Reynolds.Polymorphism constrains the power of observers by preventing them fr…
The World-Wide Web is emerging as a medium for distributing platform-independent, intermediate-form programs. Most Java vendors have recently announced plans to construct "just-in-time" systems, which translate the intermediate text into native code on demand. In this paper, we p…
This paper studies the problem of simplifying typings and the size-complexity of most general typings in typed programming languages with atomic subtyping. We define a notion of minimal typings relating all typings which are equivalent with respect to instantiation. The notion of…
Objective ML is a small practical extension of ML with objects and toplevel classes. It is fully compatible with ML; its type system is based on ML polymorphism, record types with polymorphic access, and a better treatment of type abbreviations. Objective ML allows for most featu…
As parallel machines become part of the mainstream computing environment, compilers will need to apply synchronization optimizations to deliver efficient parallel software. This paper describes a new framework for synchronization optimizations and a new set of transformations for…
We present a simple method for partitioning a dataflow analysis problem into a series of related subproblems. We use type information (either declared by the programmer, or computed via nonstandard type inference) to conservatively approximate analysis-time data dependences betwe…
We propose and study a new typing algorithm for dependent type theory. This new algorithm typechecks more terms by using inheritance between classes. This inheritance mechanism turns out to be powerful: it supports multiple inheritance, classes with parameters and uses new abstra…
Structural Operational Semantics (SOS) is a widely used formalism for specifying the computational meaning of programs, and is commonly used in specifying the semantics of functional languages. Despite this widespread use there has been relatively little work on the for such sema…
Wadler's deforestation algorithm removes intermediate data structures from functional programs. To be appropriate for inclusion in a compiler, deforestation must terminate on all programs. Several techniques exist to ensure termination of deforestation on all first-order programs…
In order to analyze a program that involves pointers, it is necessary to have (safe) information about what each pointer points to. There are many different approaches to computing points-to information. This paper addresses techniques for flow- and context-insensitive interproce…
We introduce a method for proving the correctness of transformations of programs in languages like Scheme and ML. The method consists of giving the programs a denotational semantics in an operationally-based term model in which interaction is the basic observable, and showing tha…
We present an interpretation of typed object-oriented concepts in terms of well-understood, purely procedural concepts. More precisely, we give a compositional subtype-preserving translation of a basic object calculus supporting method invocation, functional method update, and su…