Open Access. Powered by Scholars. Published by Universities.®
Programming Languages and Compilers Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Keyword
-
- Programming languages (4)
- Algol-like languages (2)
- Interference control (2)
- 25th ACM National Conference (1)
- Algol (1)
-
- Applicative language (1)
- Closure (1)
- Continuation (1)
- Functional languages (1)
- Functor-category approach (1)
- Functors (1)
- GEDANKEN (1)
- High-order function (1)
- Imperative languages (1)
- Imperative programs (1)
- Interference (1)
- Interpreter (1)
- J-operator (1)
- Java (1)
- LISP (1)
- Lambda calculus (1)
- Language definition (1)
- Logics and meanings of programs (1)
- Monitors (1)
- Observational equivalence (1)
- Order of application (1)
- PAL (1)
- Parallel programming (1)
- Programming language (1)
- Reference (1)
Articles 1 - 7 of 7
Full-Text Articles in Programming Languages and Compilers
Java’S Insecure Parallelism, Per Brinch Hansen
Java’S Insecure Parallelism, Per Brinch Hansen
College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects
The author examines the synchronization features of Java and finds that they are insecure variants of his earliest ideas in parallel programming published in 1972-73. The claim that Java supports monitors is shown to be false. The author concludes that Java ignores the last twenty-five years of research in parallel programming languages.
Definitional Interpreters For Higher-Order Programming Languages, John C. Reynolds
Definitional Interpreters For Higher-Order Programming Languages, John C. Reynolds
College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects
Abstract. Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters that are themselves written in a programming language based on the lambda calculus (i.e., an applicative language such as pure LISP). Examples include McCarthy’s definition of LISP, Landin’s SECD machine, the Vienna definition of PL/I, Reynolds ’ definitions of GEDANKEN, and recent unpublished work by L. Morris and C. Wadsworth. Such definitions can be classified according to whether the interpreter contains higher-order functions, and whether the order of application (i.e., call by value versus call by name) in the defined …
Objects, Interference, And The Yoneda Embedding, Peter W. O'Hearn, Uday S. Reddy
Objects, Interference, And The Yoneda Embedding, Peter W. O'Hearn, Uday S. Reddy
College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects
We present a new semantics for Algol-like languages that combines methods from two prior lines of development: [1] the object-based approach of [28,29], where the meaning of an imperative program is described in terms of sequences of observable actions, and [2] the functor-category approach initiated by Reynolds [31], where the varying nature of the run-time stack is explained using functors from a category of store shapes to a category of cpos. The semantics gives an account of both the phenomena of local state and irreversibility of state change. As an indication of the accuracy obtained, we present a full abstraction …
Syntactic Control Of Interference Revisited, Peter W. O'Hearn, A. J. Power, M. Takeyama, R. D. Tennent
Syntactic Control Of Interference Revisited, Peter W. O'Hearn, A. J. Power, M. Takeyama, R. D. Tennent
College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects
In "Syntactic Control of Interference" (POPL, 1978), J. C. Reynolds proposes three design principles intended to constrain the scope of imperative state effects in Algol-like languages. The resulting linguistic framework seems to be a very satisfactory way of combining functional and imperative concepts, having the desirable attributes of both purely functional languages (such as pcf) and simple imperative languages (such as the language of while programs). However, Reynolds points out that the "obvious" syntax for interference control has the unfortunate property that fi-reductions do not always preserve typings. Reynolds has subsequently presented a solution to this problem (ICALP, 1989), but …
Parametricity And Local Variables, Peter W. O'Hearn, R. D. Tennent
Parametricity And Local Variables, Peter W. O'Hearn, R. D. Tennent
College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects
We propose that the phenomenon of local state may be understood in terms of Strachey 's concept of parametric (i.e., uniform) polymorphism. The intuitive basis for our proposal is the following analogy: a non-local procedure is independent of locally-declared variables in the same way that a parametrically polymorphic function is independent of types to which it is instantiated. A connection between parametricity and representational abstraction was first suggested by J. C. Reynolds. Reynolds used logical relations to formalize this connection in languages with type variables and user-defined types. We use relational parametricity to construct a model for an Algol-like language …
Note On Algol And Conservatively Extending Functional Programming, Peter W. O'Hearn
Note On Algol And Conservatively Extending Functional Programming, Peter W. O'Hearn
College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects
A simple Idealized Algol is considered, based on Reynolds's "essence of Algol." It is shown that observational equivalence in this language conservatively extends observational equivalence in its assignment-free functional sublanguage.
A Model For Syntactic Control Of Interference, Peter W. O'Hearn
A Model For Syntactic Control Of Interference, Peter W. O'Hearn
College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects
Two imperative programming language phrases interfere when one writes to a storage variable that the other reads from or writes to. Reynolds has described an elegant linguistic approach to controlling interference in which a refinement of typed λ-calculus is used to limit sharing of storage variables; in particular, different identifiers are required never to interfere. This paper examines semantic foundations of the approach. We describe a category that has (an abstraction of) interference information built into all objects and maps. This information is used to define a “tensor” product whose components are required never to interfere. Environments are defined using …