Proofs of pointer programs in Jape

Jape's development is mostly a solitary activity. In order to make these proofs I had to extend Jape a bit (undocumented, so far), remove some inefficiencies and enhance the font I was using. For various reasons, not all of the extensions made it to the Linux version, and the font never managed to leave MacOS (once upon a time I knew how to do that, but now I've forgotten). So these proofs can only be made, for the time being, on MacOS Classic.

In order that others can read them, however, I've prepared a commentary which illustrates each proof and even includes its Japeish text. Because of that text, the commentary is huge, and I've split it into five:

1. background (47pp, 164KB), setting out much of the Japeish programming that supports the whole enterprise, including proofs of logical and data structure lemmas;
2. heap lists (36pp, 136KB), dealing with the basic => operator used to describe sequences in the heap;
3. Hoare logic and list reversal (16pp, 76KB), dealing with the encoding of Hoare logic in Jape and a proof of the list reversal program from my MPC paper;
4. list merge (65pp, 196KB), the surprisingly tricky proof of ordered list merging from the paper;
5. Schorr-Waite (152pp, 472KB), all of the proof of the famous graph-marking algorithm, with the absence of a loop measure (which I never dealt with).

If you are lucky enough to use a Mac ...