These slides summarise input sent to me by members of the Theory, Semantics and Automated Reasoning groups in the Computer Laboratory. Particular thanks to Matthew Parkinson, Larry Paulson, Andy Pitts and Peter Sewell for ideas and comments.