The use of theorem provers as fundamental aids in computer science and software engineering is slowly expanding their reach. The multitude of tools and methods does have a downside: lack of interoperability. It would be nice if, for example, proofs from one tool could be checked by another. This is a rather thorny problem because the various systems do not even agree on what is, fundamentally, a proof.

It is not even clear what the fundamental ingredients of proofs are. For any given logic, the details are clear, but it is far from obvious how much overlap there is when one changes proof technology--as the authors explain clearly, with examples and ample references. They turn to proof theory, a subdomain of mathematical logic, for inspiration. But the decisive move is to view proof checking as a combination of computation and interaction. The authors illustrate these ideas with an apt analogy of the steps required to instruct a robot on how to navigate a maze, consisting of alternative periods of intensive instructions (in areas with many obstacles) and autonomous behavior (in straight corridors). This gentle explanation of polarization from proof systems is used throughout to help the reader see through the details of each proof system, so that the common backbone emerges.

Through many examples, given in full and precise detail, the authors’ insights are used to overlay structure onto proof systems whose classical presentation is not so structured. Of course, the authors show that this harms neither soundness nor completeness when appropriate. Then, the authors proceed to add certificates to this process. These then provide the necessary evidence that can be transported to other settings. As before, these ideas are amply illustrated with a wealth of thorough examples. The theoretical insights are augmented and cemented through a complete, and available, implementation. As this implementation contains quite a few design choices, a complete section is devoted to justifying them; as a rather interesting expository choice, they expand on what would be needed if one chose (for example) to avoid the use of various features of λProlog for an implementation. As scientists, they clearly know and understand that their choices here are not inevitable; at the same time, they clearly believe that they are excellent choices.

Even though this paper is extremely well written, it is nevertheless not for the faint of heart. The full technical details of some logics are complex and notationally somewhat frightening. But these details matter, and the authors justify their thoroughness.

Anyone likely to read a paper from the Journal of Automated Reasoning should read this one. This paper is likely to have a long shelf life. Its clarity, wealth of illustrative examples, and erudition are exemplary.