This paper examines the foundational distinctions between proof theory and dependent type theory (DTT) in the design of interactive theorem provers.While several implemented systems are designed using the dependently typed λ -calculus to represent proofs, no major proof assistant is designed using modern structural proof theory, even though, as I will argue here, the sequent calculus offers a compelling alternative framework.Six specific topics are proposed where the proof-theoretic perspective is arguably superior to the DTT perspective.These topics include the separation of logic from proof structure, the strategic use of non-determinism in proof reconstruction, and the avoidance of complex typing-discipline issues such as universe levels and proof irrelevance.The final topicthe treatment of bindings-is further developed to demonstrate how a natural, intensional approach is achieved through the mobility of binders.This methodology is illustrated via the Abella theorem prover, which leverages λ -tree syntax and the ∇-quantifier to provide an elegant environment for reasoning about the meta-theory of languages and logics involving complex binding.
Dale Miller (Sat,) studied this question.