Axioms for Behavioural Congruence of Single-Pass Instruction Sequences

This is to announce the publication of a paper concerning instruction sequences. The paper entitled “Axioms for behavioural congruence of single-pass instruction sequences” (doi: 10.7561/SACS.2017.2.111) has now been published. This paper introduces a sound axiom system for behavioural congruence of single-pass instruction sequences that is complete for finite instruction sequences. This means that behavioural congruence of finite instruction sequences can now be established in a direct way by pure equational reasoning. In the past, it had to be established in an indirect way by reasoning that was not pure equational. The axiom system is especially notable for its axioms that have to do with forward jump instructions

Advertisements
Posted in Announcement of Publication | Tagged , , , , , , , | Leave a comment

Instruction Sequences Expressing Multiplication Algorithms

This is to announce an electronic preprint concerning instruction sequences, entitled “Instruction Sequences Expressing Multiplication Algorithms” (arXiv:1312.1529v3 [cs.PL]), in which “Instruction Sequence Expressions for the Karatsuba Multiplication Algorithm” (arXiv:1312.1529v2 [cs.PL]) has been combined with “Long Multiplication by Instruction Sequences with Backward Jump Instructions” (arXiv:1312.1812v3 [cs.PL]). In this preprint, we provide mathematically precise alternatives to the natural language and pseudo code descriptions of the long multiplication algorithm and the Karatsuba multiplication algorithm and establish among other things that the instruction sequence expressing the latter algorithm is shorter than the instruction sequence expressing the former algorithm only if the length of the bit strings involved is greater than 256. We also go into the use of an instruction sequence with backward jump instructions for expressing the long multiplication algorithm. This leads to an instruction sequence that it is shorter than the other two if the length of the bit strings involved is greater than 2.

Posted in Announcement of Publication | Tagged , , , , , , , , , , | Leave a comment

Axioms for Behavioural Congruence of Single-Pass Instruction Sequences

This is to announce a new version of an electronic preprint concerning instruction sequences. The paper entitled “Axioms for behavioural congruence of single-pass instruction sequences” (arXiv:1702.03511v2 [cs.PL]) has now been updated. This preprint introduces a sound axiom system for behavioural congruence of single-pass instruction sequences that is complete for finite instruction sequences. This means that behavioural congruence of finite instruction sequences can now be established in a direct way by pure equational reasoning. In the past, it had to be established in an indirect way by reasoning that was not pure equational. The axiom system is especially notable for its axioms that have to do with forward jump instructions.

Posted in Announcement of Publication | Tagged , , , , , , , | Leave a comment

Instruction Sequence Expressions for the Secure Hash Algorithm SHA-256

This is to announce a new version of an electronic preprint concerning instruction sequences. The preprint “Instruction Sequence Expressions for the Secure Hash Algorithm SHA-256” has now been updated (arXiv:1308.0219v7 [cs.PL]). In this preprint, we provide a mathematically precise alternatives to the pseudo code description of the secure hash algorithm SHA-256.

Posted in Announcement of Publication | Tagged , , , , , | Leave a comment

Instruction Sequence Expressions for the Karatsuba Multiplication Algorithm

This is to announce a new version of an electronic preprint concerning instruction sequences. The preprint “Instruction Sequence Expressions for the Karatsuba Multiplication Algorithm” has now been updated (arXiv:1312.1529v2 [cs.PL]). In this preprint, we provide mathematically precise alternatives to the natural language and pseudo code descriptions of the long multiplication algorithm and the Karatsuba multiplication algorithm and establish among other things that the instruction sequence expressing the latter algorithm is shorter than the instruction sequence expressing the former algorithm only if the length of the bit strings involved is greater than 256.

Posted in Announcement of Publication | Tagged , , , , , , , , | Leave a comment

A Hoare-Like Logic of Asserted Single-Pass Instruction Sequences

This is to announce the publication of a paper concerning instruction sequences. The paper entitled “A Hoare-like logic of asserted single-pass instruction sequences” (doi: 10.7561/SACS.2016.2.125) has now been published. In this paper, we present a Hoare-like logic that is intended to support a sound general understanding of the issues with Hoare-like logics for low-level programming languages.

Posted in Announcement of Publication | Tagged , , , , , , , , , | Leave a comment

Axioms for Behavioural Congruence of Single-Pass Instruction Sequences

This is to announce a new electronic preprint concerning instruction sequences. The paper entitled “Axioms for behavioural congruence of single-pass instruction sequences” (arXiv:1702.03511v1 [cs.PL]) has now been archived. This preprint introduces a sound axiom system for behavioural congruence of single-pass instruction sequences that is complete for finite instruction sequences. This means that behavioural congruence of finite instruction sequences can now be established in a direct way by pure equational reasoning. In the past, it had to be established in an indirect way by reasoning that was not pure equational.

Posted in Announcement of Publication | Tagged , , , , , , | Leave a comment

Instruction Sequence Size Complexity of Parity

This is to announce the publication of a paper concerning instruction sequences. The paper entitled “Instruction sequence size complexity of parity” (doi:10.3233/FI-2016-1450) has now been published. The main result of this paper supports, in a setting where programs are instruction sequences acting on Boolean registers, a basic intuition behind the storage of auxiliary data, namely the intuition that this makes possible a reduction of the size of a program.

Posted in Announcement of Publication | Tagged , , , , , , , | Leave a comment

On Instruction Sets for Boolean Registers in Program Algebra

This is to announce the publication of a paper concerning instruction sequences. The paper entitled “On instruction sets for Boolean registers in program algebra” (doi:10.7561/SACS.2016.1.1) has now been published. In this paper, we study instruction sequence size bounded functional completeness of instruction sets for Boolean registers.

Posted in Announcement of Publication | Tagged , , , , | Leave a comment

About the Site

This is to announce the replacement of the home page of this website, which is entitled “About this site”, by a substantially revised version.

Posted in Uncategorized | Tagged , , , , , , , , , | Leave a comment