The primary aim of these five technical papers is to indicate aspects of proof theory which may be of use in the study of non-numerical computing. The three main papers are entitled: "Checking of Computer Programs;""Consistency Proofs and Programs for Translators;" and "Experiments with Computers on the Complexity of Non-numerical computations." The author shows that many theorems on computability in traditional metamathematics are of little use to the computer scientist because they do not lead to feasible algorithms. He also suggests alternative approaches to proof theory which would be of greater applicability. (MM)