| One of the central goals of programming-language research is to develop mathematically sound formal methods for precisely specifying and reasoning about the behavior of programs. However, just as software developers sometimes make mistakes when programming, researchers sometimes make mistakes when proving that a formal method is mathematically sound. As the field of programming-language research has grown, these proofs have become larger and more complex, and thus harder to verify on paper. This phenomenon has motivated a great deal of research into the development of logical systems that provide an automated means to apply---and verify the application of---trusted reasoning principles to concrete proofs.;The boundary between trusted and untrusted reasoning principles is inherently blurry, and different researchers draw the line in different places. However, just as certain principles are widely recognized to allow the proofs of contradictory statements, others are so uncontroversially ubiquitous in practice that they can be considered beyond reproach. We posit the following questions: (1) what are these principles and (2) how much can we do with them?;Although neither has an uncontroversial answer, in this dissertation we propose an answer to the former by describing a philosophical viewpoint we refer to as syntactic finitism, in which the principles of case analysis and structural induction on abstract syntax are viewed as being a priori justified. We explore the latter question using some of the ideas and results from proof theory; along the way, we provide a syntactically finitary account of proofs by logical relations, and investigate the consequences of replacing structural induction with well-founded induction on the lexicographic path ordering from term rewriting theory. Finally, we argue that syntactically finitary proofs can be formalized in the proofs as logic programs paradigm popularized by the proof assistant Twelf; we prove the soundness of a modular termination-analysis that is central to the validity of this interpretation. |
