Towards the Complexity Analysis of Programming Language Proof Methods

Numerous proof methods have been proposed to establish language properties such as type soundness, confluence, strong normalization, and others. However, literature does not provide a study of the complexity of carrying out these proof methods. This paper provides an investigation on the complexity of carrying out the "syntactic approach" to type soundness (progress theorem and type preservation theorem) for a class of functional languages, and characterizes the complexity of its proofs as a function of the number of expression constructors, number of typing rules, reduction rules, and other common quantities of operational semantics. Although we do not claim to provide the complexity of this approach, this paper provides the first example of complexity analysis of a programming language proof method.