"An Introduction to Dependent Type Theory."

Gilles Barthe, Thierry Coquand (2000)
a service of Schloss Dagstuhl - Leibniz Center for Informatics