A complete mechanization of (Ω)-order type theory. - Tomasz Pietrzykowski; D. C. Jensen (ACM Annual Conference (1), 1972)

Mechanizing omega-Order Type Theory Through Unification. - D. C. Jensen; Tomasz Pietrzykowski (Theor. Comput. Sci., 1976)