POPL

This paper proposes an expressional loop notation (XLoop) based on the ideas described in [16,17] which makes it practical to express loops as compositions of functions. The primary benefit of XLoop is that it brings the powerful metaphor of expressions ...

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. ...

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-...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

Inverse currying transformation of an attribute grammar moves a context condition to places in the grammar where the violation of the condition can be detected as soon as the semantic information used in the condition is computed. It thereby takes into ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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” ...

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 λ-calculus. Procedures are entirely explained at a purely ...

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 ...

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 ...

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 ...