"Object-oriented programming in dependent type theory."

Anton Setzer (2006)
a service of Schloss Dagstuhl - Leibniz Center for Informatics