2,199 papers · page 97 of 110
Article Free Access Share on An ideal model for recursive polymorphic types Authors: David MacQueen Bell Laboratories, Murray Hill, New Jersey Bell Laboratories, Murray Hill, New JerseyView Profile , Gordon Plotkin Department of Computer Science, University of Edinburgh, Edinburg…
We have developed a complete formal specification of the translation semantics of the Pascal P-compiler. The specification is written as a semantic grammar (a variant of extended attribute grammars), and has been extensively tested and debugged with the aid of Lawrence Paulson's …
An applicative program denotes a function mapping values from some domain to some range. Abstract interpretation of applicative programs involves using the standard denotation to describe an abstract function from a “simplified” domain to a “simplified” range, such that computati…
A simple semantic model of automatic coercion is proposed. This model is used to explain four rules for inferring polymorphic types and providing automatic coercions between types. With the addition of a fifth rule, the rules become semantically complete but the set of types asso…
The conventional storage allocation scheme for block structured languages requires the allocation of stack space and the building of a display with each procedure call. This paper describes a technique for analyzing the call graph of a program in a block structured language that …
Article Efficient applicative data types Share on Author: Eugene W. Myers Department of Computer Science, The University of Arizona, Tucson, Arizona Department of Computer Science, The University of Arizona, Tucson, ArizonaView Profile Authors Info & Claims POPL '84: Proceedings …
An editing by example system is an automatic program synthesis facility embedded in a text editor that can be used to solve repetitive text editing problems. The user provides the editor with a few examples of a text transformation. The system analyzes the examples and generalize…
Article Grids: A new program structuring mechanism based on layered graphs Share on Author: Harold L. Ossher Computer Science Department, Stanford University, Stanford, CA Computer Science Department, Stanford University, Stanford, CAView Profile Authors Info & Claims POPL '84: P…
A defining characteristic of “functional” specifications is the absence of assignments: updates of tables and data structures are expressed by giving the relationship between the new and old values. An obvious implementation allocates separate space for new and old values and may…
Knowledge of logical inference rules allows a specialized proof editor to provide a user with feedback about errors in a proof under development. Providing such feedback involves checking a collection of constraints on the strings of the proof language. Because attribute grammars…
Treat is a special purpose language for use in compiler writing. A Treat program translates a graph into c-trees (the intermediate language of the pcc compiler) and uses the back end of the C compiler to generate code. Treat has been developed specifically for use in an AdaTM com…
Concurrent Prolog [28] combines the logic programming computation model with guarded-command indeterminacy and dataflow synchronization. It will form the basis of the Kernel Language [21] of the Parallel Inference Machine [36], planned by Japan's Fifth Generation Computers Projec…
We examine local area network protocols and verify the correctness of two representative algorithms using temporal logic. We introduce an interval temporal logic that allows us to make assertions of the form “in the next k units, X holds.” This logic encodes intuitive arguments a…
Article Free Access Share on Paragon: Novel uses of type hierarchies for data abstraction Author: Mark Sherman Department of Math. and Computer Science, Dartmouth College, Hanover, NH Department of Math. and Computer Science, Dartmouth College, Hanover, NHView Profile Authors Inf…
A novel lazy evaluation mechanism, pattern-driven lazy reduction, is developed that serves as a unifying evaluation mechanism for both functional and logic programs. The reduction of a function call can be viewed as “semantically” unifying the function call with the left hand sid…
Increasingly computer science research has been done using workstations with high-resolution bitmap display systems. Smalltalk-80↑ is a very attractive programming language for such computation environments, since it has very sophisticated graphical systems and programming enviro…
We give an algorithm to test the completeness of definitions holding on the rewrite systems that they generate. At the opposite of existing techniques that are very restrictive (left-hand sides of definitions must be linear) or rather inefficient our solution is both powerful and…
In this paper we present a semantics for Milner-style polymorphism in which types are sets. The basic picture is that our programs are actually terms in a typed λ-calculus, in which the type information can be safely deleted from the concrete syntax. In order to allow for common …
In this paper, we propose a new dependence baaed program representation.This representation is the union of two previously separate concepts: loop carried dependence and hierarchical abstraction.The resulting form has the property that all information necessary to reorder the set…