This is a tutorial on backend programming for holpy, which can also serve as an introduction to higher-order logic. The tutorial consists of a series of Jupyter notebooks, and can be viewed using nbviewer.
This tutorial is under active development. New material will be added on a regular basis.