Techniques of computable set theory with applications to proof verification