On Definition Trees of Ordinal Recursive Functonals: Reduction of the Recursion Orders by Means of Type Level Raising. - Jan Terlouw (J. Symb. Log., 1982)

Reduction of higher type levels by means of an ordinal analysis of finite terms. - Jan Terlouw (Ann. Pure Appl. Log., 1985)

Algebraic Proof Assistants in HOL. - Rix Groenboom; Chris Hendriks; Indra Polak; Jan Terlouw; Jan Tijmen Udding (MPC, 1995)

Strong Normalization in Type Systems: A Model Theoretic Approach. - Jan Terlouw (Ann. Pure Appl. Log., 1995)