On the programs-as-formulas interpretation of parallel programs in Peano arithmetic (Q1100878)

The reviewed paper concerns the representation of some parallel programs by formulas of the Peano arithmetic (PA). The main part of the paper is devoted to the definitions of the programming language, program types, tagged and untagged execution schemes, the next-node tree associated with a program and an input, programs as formulas of PA, next value relation, deadlock-free programs and correctness property, completed by numerous examples. The main theoretical results are concentrated in two rather obvious theorems on the definability of the next value relation in PA and the correctness of the considered type of deadlock-free programs.