Polynomial-time Martin-Löf type theory
fragments of extensional Martin-Löf type theory without universes
scientific article; zbMATH DE number 438613