A correspondence between Martin-Löf type theory, the ramified theory of types and pure type systems

DOI10.1023/A:1011286100450zbMath0977.03011MaRDI QIDQ5939957

Fairouz Kamareddine, Twan Laan

Publication date: 23 July 2001

Published in: Journal of Logic, Language and Information (Search for Journal in Brave)

zbMATH Keywords

ordersMartin-Löf's Type Theoryproof checker Nuprlpure type systemsRussell's Ramified Theory of Types

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35)

Uses Software

• Nuprl
• Automath
• Unnamed Item

This page was built for publication: A correspondence between Martin-Löf type theory, the ramified theory of types and pure type systems