Trying to go through and adapt Frank and Iliano's LLF miniml type preservation proof to the HLF implementation. The modes of the higher-order thingies having to do with reference cells are slightly more subtle than I expected, but once I understand what they're supposed to do it's all quite lovely, actually.
For any of you that enjoyed Schild's Ladder, I might recommend taking a look at Spin Networks, the thing Egan's fictional "Quantum Graph Theory" was clearly based on. I found the original Penrose paper on the topic to be astonishingly readable up until about page 26 when he starts talking about 'twistors', which are to SU(2,2) and SO(2,4) what spinors are to SU(2) and SO(3). Also this is a more recent tutorial paper with another crop of pretty diagrams.
For any of you that enjoyed Schild's Ladder, I might recommend taking a look at Spin Networks, the thing Egan's fictional "Quantum Graph Theory" was clearly based on. I found the original Penrose paper on the topic to be astonishingly readable up until about page 26 when he starts talking about 'twistors', which are to SU(2,2) and SO(2,4) what spinors are to SU(2) and SO(3). Also this is a more recent tutorial paper with another crop of pretty diagrams.