Type theory and formal proof an introduction - Nederpelt, Rob; Geuvers, Herman (Cambridge University Press, 2014)