“Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over several years of teaching a freshman-level course, ‘Logic and Computation,’ to thousands of undergraduate students. In our companion paper, we presented our calculational proof format [and] gave an overview of the calculational proof checker (CPC) tool that we developed. … In this paper, we dive deeper into the implementation details of CPC, highlighting how proof validation works, which helps us argue that our proof checking process is sound.”

Find the paper and authors list at ArXiv.