J. A. Bergstra
We introduce a process algebra that concerns the timed behaviour of distributed systems with a known spatial distribution. This process algebra provides a communication mechanism that deals with the fact that a datum sent at one point in…
This paper concerns the relation between process algebra and Hoare logic. We investigate the question whether and how a Hoare logic can be used for reasoning about how data change in the course of a process when reasoning equationally about…
In process algebras such as ACP (Algebra of Communicating Processes), parallel processes are considered to be interleaved in an arbitrary way. In the case of multi-threading as found in contemporary programming languages, parallel processes…
Many public controversies involve the assessment of statements about which we have imperfect information. Without a structured approach, it is quite difficult to develop an approach to reasoning which is not based on ad hoc choices. Forms…
This paper presents an algebraic theory of instruction sequences with instructions for Turing tapes as basic instructions, the behaviours produced by the instruction sequences concerned under execution, and the interaction between such…
This paper concerns the question to what extent it can be efficiently determined whether an arbitrary program correctly solves a given problem. This question is investigated with programs of a very simple form, namely instruction sequences,…
In program algebra, an algebraic theory of single-pass instruction sequences, three congruences on instruction sequences are paid attention to: instruction sequence congruence, structural congruence, and behavioural congruence. Sound and…
A parameterized algebraic theory of instruction sequences, objects that represent the behaviours produced by instruction sequences under execution, and objects that represent the behaviours exhibited by the components of the execution…
For each function on bit strings, its restriction to bit strings of any given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump…
The secure hash function SHA-256 is a function on bit strings. This means that its restriction to the bit strings of any given length can be computed by a finite instruction sequence that contains only instructions to set and get the…
We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial correctness of segments of the single-pass instruction…
In a previous paper, an ACP-style process algebra was proposed in which propositions are used as the visible part of the state of processes and as state conditions under which processes may proceed. This process algebra, called ACPps, is…
Each Boolean function can be computed by a single-pass instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. Auxiliary Boolean…
In previous work carried out in the setting of program algebra, including work in the area of instruction sequence size complexity, we chose instruction sets for Boolean registers that contain only instructions of a few of the possible…
Meadows are alternatives for fields with a purely equational axiomatization. At the basis of meadows lies the decision to make the multiplicative inverse operation total by imposing that the multiplicative inverse of zero is zero. Divisive…
We add probabilistic features to basic thread algebra and its extensions with thread-service interaction and strategic interleaving. Here, threads represent the behaviours produced by instruction sequences under execution and services…
Every partial function from bit strings of a given length to bit strings of a possibly different given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers,…
Meadows have been proposed as alternatives for fields with a purely equational axiomatization. At the basis of meadows lies the decision to make the multiplicative inverse operation total by imposing that the multiplicative inverse of zero…
This paper concerns instruction sequences that contain probabilistic instructions, i.e. instructions that are themselves probabilistic by nature. We propose several kinds of probabilistic instructions, provide an informal operational…
We present an approach to non-uniform complexity in which single-pass instruction sequences play a key part, and answer various questions that arise from this approach. We introduce several kinds of non-uniform complexity classes. One kind…