An information system interpretation of Martin-Löf's partial type theory with universes
scientific article; zbMATH DE number 465563