Faculty position in PL/verification/theorem-proving at Cambridge.