Impredicativity entails Untypedness. - Peter Lietz; Thomas Streicher (Math. Struct. Comput. Sci., 2002)

Realizability models refuting Ishihara's boundedness principle. - Peter Lietz; Thomas Streicher (Ann. Pure Appl. Log., 2012)