Basic Simple Type Theory
J. Roger Hindley