Intuitionistic Type Theory

Author — Per Martin-Lof