Ein ausgezeichnetes Modell für die intuitionistische Typenlogik. Wilfried Buchholz (1975) Archiv für mathematische Logik und Grundlagenforschung
Ein starker Normalisationssatz für die bar-rekursiven Funktionale. Helmut Vogel (1977) Archiv für mathematische Logik und Grundlagenforschung
Ein starker Normalisationssatz für die intuitionistische Typentheorie. Wolfram Pohler (1973) Manuscripta mathematica
Ein syntaktischer Beweis für die Zulässigkeit der Schnittregel im Kalkül von Schütte für die intuitionistische Typenlogik. Horst Osswald (1973) Manuscripta mathematica