A formalisation of the ideas in this sequence in higher-order logic, including machine verified proofs of all the theorems, is available here.
A formalisation of the ideas in this sequence in higher-order logic, including machine verified proofs of all the theorems, is available here.