"Typechecking Dependent Types and Subtypes."

Luca Cardelli (1986)
a service of Schloss Dagstuhl - Leibniz Center for Informatics