2,199 papers · page 105 of 110
Interesting program properties other than functional correctness can be addressed and proved using axiomatic logic. An information flow logic that defines the flow semantics of a parallel programming language is presented. Proofs in this logic can be used to certify programs with…
A linear recursive procedure is one in which a procedural call can activate at most one other procedural call. When linear recursion cannot be replaced by iteration, it is usually implemented with a stack of size proportional to the depth of recursion. In this paper we analyze im…
SETL is a very high level programming language supporting set theoretical syntax and semantics. It allows algorithms to be programmed rapidly and succinctly without requiring data structure declarations to be supplied, though such declarations can be manually specified later, wit…
In this paper we describe how Lucid can be extended to allow user-defined functions and scope conventions, i.e. conventions for limiting the range or scope of the validity of definitions. This is done using new constructs called clauses which are similar in form to the blocks and…
This paper presents a new version of Hoare's logic including generalized procedure call and assignment rules which correctly handle aliased variables. Formal justifications are given for the new rules.
The model of abstract interpretation of programs developed by Cousot and Cousot [2nd ISOP, 1976], Cousot and Cousot [POPL 1977] and Cousot [PhD thesis 1978] is applied to the static determination of linear equality or inequality invariant relations among numerical variables of pr…
The parallelity means "simultaneous performance or execution" and it may concern either computer units of different sorts (e.g. a memory and a processor), or computer units of the same sort (e.g. several processors).The computers Illiac 4 and Burroughs Scientific Processor (BSP) …
This paper describes a novel approach to the treatment of data types in programming languages, which allows a simple interpretation of "polymorphic" or "generic" procedures, makes a simple set of type-checking rules semantically justifiable and provides a straightforward treatmen…
The classical common subexpression problem in program optimization is the detection of identical subexpressions. Suppose we have some extra information and are given pairs of expressions ei1=ei2 which must have the same value, and expressions fj1≠fj2 which must have different val…
The Runcheck Verifier is a working system for proving the absence of common runtime errors. The language accepted is Pascal without variant records, side effects in functions, shared variable parameters to procedures, or functional arguments. The errors checked are: 1) accessing …
An algorithm is given to translate a relatively low-level intermediate representation of a program into assembly code or machine code for a target computer. The algorithm is table driven. A construction algorithm is used to produce the table from a functional description of the t…
Article Free Access Share on A Metalanguage for interactive proof in LCF Authors: M. Gordon University of Edinburgh University of EdinburghView Profile , R. Milner University of Edinburgh University of EdinburghView Profile , L. Morris Syracuse University Syracuse UniversityView …
Most existing APL implementations are interpretive in nature, that is, each time an APL statement is encountered it is executed by a body of code that is perfectly general, i.e. capable of evaluating any APL expression, and is in no way tailored to the statement on hand. This cos…
A partial evaluation program for LISP is described, and an application where it has been used. The partial evaluator performs a number of other, related operations such as opening of functions and certain optimizations on programs. The application is based on the fact that we can…
We investigate the principles underlying reasoning about nondeterministic programs, and present a logic to support this kind of reasoning. Our logic, an extension of dynamic logic ([22] and [12]), subsumes most existing first-order logics of nondeterministic programs, including t…
This paper describes a programming system based on the metaphor of communicating objects. Experience with a running system shows that this model provides flexibility, modularity and compactness. A compiled representation for the language is presented, along with an interpreter su…
A compiler for the C language has recently been constructed which is now compiling C for about half a dozen machines. The compiler was influenced in various ways by recent theoretical developments. This paper gives an overview of the compiler structure and algorithms, emphasizing…
The method of local constraints attempts to describe context-free languages in an apparently context-sensitive form which helps to retain the intuitive insights about the grammatical structure. This form of description, while apparently context-sensitive is, in fact, context-free…
We present the best known algorithm for the determination of run-time types in a programming language requiring no type declarations. We demonstrate that it is superior to other published algorithms and that it is the best possible algorithm from among all those that use the same…
Data flow programming languages are especially amenable to mathematization of their semantics in the denotational style of Scott and Strachey. However, many real world programming problems, such as operating systems and data base inquiry systems, require a programming language ca…