Investigating a proof-theoretic meta-language for functional programs
John Hannan, Dale Armin Miller · ScholarlyCommons (University of Pennsylvania) · 1990
In this dissertation we study a higher-order intuitionistic logic used as a specification language for a variety of tasks that treat functional programs as data objects. Such meta-programming tasks offer unique challenges including the representation of programs as data objects and the analysis of these objects. We present a technique, inspired by natural semantics and structural operational semantics, for specifying properties of programs. Specifications of this sort are presented as sets of inference rules and are encoded as clauses in a higher-order, intuitionistic meta-logic. Programs are represented by $\\lambda$-terms and many features of the language such as lexical scoping are enforced through the use of $\\lambda$-abstractions. Program properties are represented as propositions over these terms and are then proved by constructing proofs in our meta-logic. This meta-logic, based on natural deduction, includes inference rules for the introduction and discharge of both hypotheses and eigenvariables. We demonstrate how these rules provide simple and elegant manipulations of bound variables in functional programs. We also demonstrate how transforming proofs and proof systems in this setting provides a means for transforming meta-programs, producing new meta-programs that have certain desired properties or behaviors. We argue the following points regarding these specifications and their proofs: (i) the specifications of numerous meta-programming tasks are clear, concise and well structured, providing them with simple explanations and correctness proofs; (ii) a wide variety of meta-programming tasks can be specified in a single unified framework, and thus we can investigate and understand the relationship between various tasks; (iii) proofs describing computations or other kinds of manipulations provide a structure that can be analyzed, using established techniques from proof theory; (iv) specifications in our logic have a direct translation to programs in the logic programming language $\\lambda$Prolog and this translation provides a mechanism for producing experimental implementations of our meta-programs.