Haskell is a functional programming language whose evaluation is lazy by default. However, Haskell also provides pattern matching facilities which add a modicum of eagerness to its otherwise lazy default evaluation. This mixed or “non-strict” semantics can be quite difficult to reason with. This paper introduces a programming logic, P -logic, which neatly formalizes the mixed evaluation in Haskell pattern-matching as a logic, thereby simplifying the task of specifying and verifying Haskell programs. In p -logic, aspects of demand are reflected or represented within both the predicate language and its model theory, allowing for expressive and comprehensible program verification.

The familiar Hindley-Milner type system of the ML language family is extended with monad annotations to account for possible side effects of expression evaluation. This also allows effects to be effectively encapsulated by lexical scopes Γ with enforcement provided by type checking. A type-and-effects analysis supports type inference. Type soundness and completeness theorems establish the coherence of monadic type inference with the reference semantics of a small ML-style language.

The G-machine is a language-directed processor architecture designed to support graph reduction as a model of computation. It can carry out lazy evaluation of functional language programs and can evaluate programs in which logical variables are used. To support these language features, the abstract machine requires tagged memory and executes some rather complex instructions, such as to evaluate a function application.This paper explores an implementation of the G-machine as a high performance RISC architecture. Complex instructions can be represented by RISC code without experiencing a large expansion of code volume. The instruction pipeline is discussed in some detail. The processor is intended to be integrated into a standard, 32-bit memory architecture. Tagged memory is supported by aggregating data with tags in a cache.

There are two important notions of types being used in programming languages today. In the concept called types, types are algebras; the semantics of programs is described in terms of operations in these algebras. Another notion of found in most of the typed programming languages in actual use regards types as sets of objects; the elements of types are the objects manipulated by the operators of a programming language. I shall be careful to use abstract when I mean the algebraic notion, and data or simply type to mean the set-based concept.This paper presents a formal theory of types as an approximation to the exact semantics of a language, following the lead of Milner [Mil78]. The semantics is based upon multi-sorted algebras [ADJ73, 76, 77, 78] and is applied to a language consisting of equational specifications that define an type. The principal results of the paper are to characterize a class of typings as uniform approximations to an exact semantics, to extend Milner's theory of types to include types formed by coproduct construction, and to explicate typing as an (approximate) semantics for an equational theory.In developing a formal theory of types as multi-sorted algebras, the word is used to designate names used to distinguish various sets of objects that may constitute the domains of operators. Sorts are thus analogous to types in programming languages. However, the sort signatures given to operators of types do not themselves constitute a very richly descriptive language. Sort names can be formed into sequences, corresponding to product construction in an object domain, but the theory (multi-sorted Σ-algebras) does not seem to allow alternation sequences of sorts, corresponding to coproduct construction in an object domain. If this were possible, then sort signatures could actually fulfill the role of types. We shall see that alternation sequences in signatures arise naturally as a consequence of the semantics given to an equational theory.

data types, and in particular those that are designed to provide resources for use by concurrently executable programs, are often designed to be used only in certain ways.The intended constraints on use of an instance of such a type can be expressed in two principal ways: as assertions on the domain of values input to each operator, and as constraints on the sequences in which the operators of the type can be called by a customer process.These constraints must be enforced in the environment in which an instance of the type is used.Nevertheless, they are very much a part of the type specification, for its definition is not complete, nor can the consistency of its representation be proved, without them.A notation is provided in which to express sequential constraints, which are here called accessright expressions.It is suggested that these expressions should be declared in a programming language that supports the definition of monitors or resource managers.Implications for the proof rules of monitors are discussed, and suggestions are made for a programming language implementation.

In Concurrent Pascal, an explicit hierarchy of access rights to abstract variables is stated in the program text and checked by the compiler. This declarative control of static access rights provides a considerable degree of protection against unauthorized use of an abstract variable by an errant program component. However, there are cases in which the mechanism of Concurrent Pascal falls short of enforcing the principle that each program component should have within its name space only those rights of access to variables that it requires. This paper outlines an extension to the static access control mechanism of Concurrent Pascal that can enforce the need-to-know principle.

Described is a method for syntactic error recovery that is compatible with deterministic parsing methods and that is able to recover from many errors more quickly than do other schemes because it performs global context recovery. The method relies on fiducial symbols, which are typically reserved key words of a language, to provide mileposts for error recovery. The method has been applied to LL(1) parsers, for which a detailed algorithm is given, and informally proved correct. The algorithm will always recover and return control to the parser if the text being analyzed satisfies only minimal requirements: that it contains one or more occurrences of fiducial symbols following the point at which an error is detected. Tables needed for error recovery have been automatically generated, along with parsing tables, by a parser constructor for the LL(1) grammars. A theoretical characterization of fiducial symbols is given, and the utility of this characterization in practice is discussed. It has been applied to a grammar for the programming language Pascal to aid in selection of a set of fiducial symbols. The error recovery scheme has been tested on a set of student-written Pascal program texts and is compared with other error recovery strategies.

In his recent paper, “Communicating Sequential Processes” ( Comm. ACM 21, 8 (Aug. 1978), 666-677), C.A.R. Hoare outlines a programming language notation for interprocess communication in which processes are synchronized by the messages they exchange. The notation carries with it certain implications for the synchronization protocols required in a message transfer. These are not at all obvious and are made explicit here. An alternative convention is suggested in which communication and synchronization are partially uncoupled from one another.

The use of capabilities to control the access of component programs to resources in an operating system is an attractive means by which to provide a uniform protection mechanism. In this paper, a capability is defined as an abstract encapsulation of the data needed to define access to a protected object. We do not assume that capability checking is necessarily concentrated in a protection kernel, nor that capabilities to different types of objects are all of the same degree of complexity. We explore a language-based capability mechanism in which protection environments are established by declaration, enforcement protocols are automatically produced by a compiler, and access control policy is clearly placed in the hands of the system designer. The basic mechanism introduced is a program component called a capability manager that is an extension of the monitor concept. It can be used to realize most of the facilities associated with kernel-based capabilities, including preemptive revocation.

In Concurrent Pascal, the syntactic and semantic definition of the language prevents the inadvertent definition of a program that might violate the integrity of a shared data object. However, the language also does not allow the dynamic allocation of reusable resources among processes, and this restriction seems unnecessarily stingent. This paper proposes the addition to Concurrent Pascal of a new type of program component, to be called a resource manager. By this means, dynamic resource allocation can be accomplished both safely and efficiently. The notion that a process holds access rights to a resource is generalized to the notion that it holds capability rights, but the capability to atually make use of a resource is granted dynamically. The anonymity of dynamically allocatable resources is also guaranteed.

This paper studies a number of logically complete search strategies (refinements) for improving the performance of automatic theorem-proving programs based on the resolution principle. These strategies restrict the number of deductions generated by the program at the expense of sometimes missing the shortest proof. By considering elementary proof-preserving transformations on resolution proof trees, (i) it is shown that the conjunction of set-of-support, resolution-with-merging, and linear form deduction is again a complete refinement; (ii) bounds are obtained on the possible increase in complexity of the proof trees when the linear form and resolution-with-merging refinements are imposed. Finally, examples are given which demonstrate the savings in time and storage when refinements are used to prove some theorems of moderate difficulty in group theory and ternary boolean algebra.