A construction of type: type in Martin-Löf's partial type theory with one universe

DOI10.2307/2275068zbMath0747.03027OpenAlexW4241070479MaRDI QIDQ3985097

Erik Palmgren

Publication date: 27 June 1992

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2275068

zbMATH Keywords

fixed point operatorpartial type theoryimpredicativityMartin-Löf's inconsistent type theory

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35)

Related Items (3)

Dependent products and 1-inaccessible universes ⋮ The paradox of trees in type theory ⋮ Remarks on Martin-Löf's partial type theory

This page was built for publication: A construction of type: type in Martin-Löf's partial type theory with one universe