2,199 papers · page 96 of 110
Logic programming offers a variety of computational effects which go beyond those customarily found in functional programming languages. Among these effects is the notion of the “logical variable.” i.e. a value determined by the intersection of constraints, rather than by direct …
Conventional Milner-style polymorphic type checkers automatically infer types of functions and simple composite objects such as tuples. Types of recursive data structures (e.g. lists) have to be defined by the programmer through an abstract data type definition. In this paper, we…
Article Free Access Share on Abstract types have existential types Authors: John C. Mitchell AT&T Bell Laboratories, Murray Hill, New Jersey AT&T Bell Laboratories, Murray Hill, New JerseyView Profile , Gordon D. Plotkin Department of Computer Science, University of Edinburgh, Ed…
A model and a sound and complete proof system for networks of processes in which component processes communicate exclusively through messages is given. The model, an extension of the trace model, can describe both synchronous and asynchronous networks. The proof system uses tempo…
This paper considers current solutions to the problem of representing multiple environments, and uses the results to develop a new model. The motivation is partly a consequence of the renewed interest in the more sophisticated forms of access and control [Sussman & Steele 1978], …
Although optimizing compilers have successfully been used to reduce the size and running times of compiled programs, present incremental compilers only support the incremental update of unoptimized code. In this work, we extend the notion of incremental compilation to include opt…
An attempt is made to apply ideas about algebraic specification in the context of a programming language. Standard ML with modules is extended by allowing axioms in module interface specifications and in place of code. The resulting specification language, called Extended ML, is …
With current compiler technology, changing a single line in a large software system may trigger massive recompilations. If the change occurs in a file with shared definitions, all compilation units depending upon that file must be recompiled to assure consistency. However, many o…
We show how a programming language designer may embed the type structure of a programming language in the more robust type structure of the typed lambda calculus. This is done by translating programs of the language into terms of the typed lambda calculus. Our translation, howeve…
Constant propagation is a well-known global flow analysis problem. The goal of constant propagation is to discover values that are constant on all possible executions of a program and to propagate these constant values as far forward through the program as possible. Expressions w…
Up to this point direct implementations of axiomatic or equational specifications have been limited because the implementation mechanisms used are incapable of capturing the full semantics of the specifications. The programming language Unicorn was designed and implemented with t…
The Smalltalk-80* programming language includes dynamic storage allocation, full upward funargs, and universally polymorphic procedures; the Smalltalk-80 programming system features interactive execution with incremental compilation, and implementation portability. These features…
We present a generalization of the known fairness and equifairness notions, called @@@@-fairness, in three versions: unconditional, weak and strong. For each such version, we introduce a proof rule for the @@@@-fair termination induced by it, using well-foundedness and countable …
In this paper a generalization of a certain Lipton's theorem (see Lipton [5]) is presented. Namely, we show that for a wide class of programming languages the following holds: the set of all partial correctness assertions true in an expressive interpretation I is uniformly decida…
Clarke has shown that it is impossible to obtain a relatively complete axiomatization of a block-structured programming language if it has features such as static scope, recursive procedure calls with procedure parameters, and global variables, provided that we take first-order l…
Denotational semantics for an ALGOL-like language with finite-mode procedures, blocks with local storage, and sharing (aliasing) is given by translating programs into an appropriately typed l-calculus. Procedures are entirely explained at a purely functional level - independent o…
This paper summarizes a project, introduced in [HO79, HO82b], whose goal is the implementation of a useful interpreter for abstract equations that is absolutely faithful to the logical semantics of equations. The Interpreter was first distributed to Berkeley UNIX VAX sites in May…
Article Free Access Share on A combinator-based compiler for a functional language Authors: Paul Hudak Yale University, Department of Computer Science Yale University, Department of Computer ScienceView Profile , David Kranz Yale University, Department of Computer Science Yale Un…
This paper adapts applicative programming techniques to the synthesis of mynchronaua system descriptions.It presents a unifying perspective on hardware and software engineering and shows that a functional design paradigm is suitable in both realms.Established techniques for progr…
Article Completion of a set of rules modulo a set of equations Share on Authors: Jean-Pierre Jouannaud CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE) CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE)View Profile , Helene Kirchner CRIN, BP 239, 54506 Vandoeuvre le…