7,482 papers · page 296 of 375
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 address the problem of dependency analysis and caching in the context of the λ-calculus. The dependencies of a λ-term are (roughly) the parts of the λ-term that contribute to the result of evaluating it. We introduce a mechanism for keeping track of dependencies, and discuss h…
In this paper we prove time and space bounds for the implementation of the programming language NESL on various parallel machine models. NESL is a sugared typed λ-calculus with a set of array primitives and an explicit parallel map over arrays. Our results extend previous work on…
Synchronous data-flow is a programming paradigm which has been successfully applied in reactive systems. In this context, it can be characterized as some class of static bounded memory data-flow networks. In particular, these networks are not recursively defined, and obey some ki…
The designs and implementations of efficient aggregate data structures have been important issues in functional programming. It is not clear how to select a good representation for an aggregate when access patterns to the aggregate are highly variant, or even unpredictable. Previ…
Mixin modules are proposed as a new construct for module languages, allowing recursive definitions to span module boundaries. Mixin modules are proposed specifically for the Standard ML language. Several applications are described, including the resolution of cycles in module imp…