Reasoning in a logic with definitions and induction

We present a logic for the specification and analysis of deductive systems. This logic is an extension of a simple intuitionistic logic that admits higher-order quantification over simply typed $\lambda$-terms. These are key ingredients for higher-order abstract syntax, an elegant and declarative treatment of object-level abstraction and substitution. The logic also supports induction and a notion of definition. The latter concept of definition is a proof-theoretic device that allows certain theories to be treated as closed or as defining fixed points. We prove that cut-elimination and consistency results hold for this logic, adapting a technique due to Tait and Martin-Lof. We also demonstrate the effectiveness of the logic for encoding meta-level predicates such as bisimulation and for reasoning about judgements encoded using higher-order abstract syntax. The sense of closure in definitions allows us to clearly express the notions of simulation and bismulation, and we derive in our logic some high-level properties about these notions in the context of abstract transition systems. Formal meta-theoretic analysis of higher-order abstract syntax encodings has been inadequately addressed in previous research. We explore the difficulties of this task by considering encodings of intuitionistic and linear logics, and formally derive the admissibility of cut for important subsets of these logic. We then propose an approach to avoid the apparent tradeoff between the benefits of higher-order abstract syntax and the ability to analyze the resulting encodings. We illustrate this approach through examples involving the simple functional and imperative programming languages PCF and PCF$\sb{:=}.$ We formally derive such properties as unicity of typing, subject reduction, determinacy of evaluation, and the equivalence of transition semantics and natural semantics presentations of evaluation