I haven't read any of these but they might be useful:

Some [notes of Frank Pfenning][1].

A [paper of Wirth][2].


  [1]: http://www.cs.mcgill.ca/~bpientka/courses/comp527/handouts/atp.pdf
  [2]: https://arxiv.org/abs/0902.3294