Proof Theory and Dependent Type Theory: Distinct Foundations for Designing Proof Assistants

Dale Miller

This paper examines the foundational distinctions between proof theory and dependent type theory (DTT) in the design of interactive theorem provers. While several implemented syste…