The aim of the paper is to describe an extension of the notion of soft typing which increases its usefulness in software engineering. Our soft typing concept is general enough to be integrated into a wide variety of normal languages, including formalizations of mathematics, with a view to increasing reasoning productivity in the development of verified software. Specifically the paper extends the concept of soft typing to general first order languages in a parametric many sorted framework. Conventionally static and dynamic type checking are treated rather separately and so do not achieve the full potential of the typing concept. Soft typing embeds both static and dynamic type checking within a uniform framework, to provide a more efficient and flexible type checking method. For example soft typing allows incremental type extensions within a theory to be justified by discharging appropriate proof obligations within that theory. Incremental static and dynamic checking is also supported.

Abstract In many areas of computation and reasoning, the value of an expression may depend on an implicit parameter, which may for example represent a program state, or time, or a possible world. In this paper we describe a formal first order logic which captures a general notion of expressions which depend on an implicit parameter. Both semantics and syntax are discussed. An important application of the logic, used as a running example, is to provide a basis for unifying the Hoare logic of procedural programs with the mathematically powerful techniques of classical logic and set theory. It is, however, beyond the scope of this paper to develop this application fully.

Traditionally, mathematical logic has been content with ‘in principle’ formalizations of deductive inference, which place little emphasis on the description of practical reasoning. Requirements for formal descriptions of practical inference methods are now emerging however. For example, interactive reasoning systems are needed for verification of computer systems, and should support practically convenient reasoning techniques as strongly as possible. This paper describes a proof paradigm which formalises a hierarchical, problem-reduction style of reasoning which is widely useful in practical reasoning. It is a goal directed paradigm, which gives a central role to equivalence transformations. A hierarchy of subgoals can co-exist at a single point in the proof, and these subgoals may be of arbitrary type. The approach allows good access to contextual information when transforming subgoals, and can be applied to a variety of logics.

Criteria for adequacy of a data flow semantics are discussed and Kahn's successful semantics for functional (deterministic) data flow is reviewed. Problems arising from nondeterminism are introduced and the paper's approach to overcoming them is introduced. The approach is based on generalizing the notion of input-output relation, essentially to a partially ordered multiset of input-output histories. The Brock-Ackerman anomalies concerning the input-output relation model of nondeterministic data flow are reviewed, and it is indicated how the proposed approach avoids them. A new anomaly is introduced to motivate the use of multisets. A formal theory of asynchronous processes is then developed. The main result is that the operation of forming a process from a network of component processes is associative. This result shows that the approach is not subject to anomalies such as that of Brock and Ackerman.

A constructive version of Morse set theory is given, based on Heyting's predicate calculus and with countable rather than full choice. An elaboration of the method of [5] is used to show that the theory is combinator-realizable in the sense defined there. The proof depends on the assumption of the syntactic consistency of the theory. The method is introduced by first treating a subtheory without countable choice of foundation. It is intended that the work can be read either classically or constructively, though whether the word constructive is correctly used as a description of either the theory or the metatheory is of course a matter of opinion.