David Baelde (in collaboration with Gopalan Nadathur and Alwen Tui) taught an ESSLLI 2012 Introductory Course in the Logic and Computation track titled “Specification and Prototyping Using Higher Order Logic”. His lectures involved using many of the ideas and systems that involve the Parsifal team: the Teyjus implementation of λProlog and the Bedwyr and Abella systems. Course information is available as are his lecture notes.