The ALF Proof Editor and Its Proof Engine. - Lena Magnusson; Bengt Nordström (TYPES, 1993)

An Algorithm for Checking Incomplete Proof Objects in Type Theory with Localization and Unification. - Lena Magnusson (TYPES, 1995)