A Framework for Reasoning About LF Specifications

Abstract

With growing reliance on software in the modern world there is also a growing interest in ensuring that these systems behave in desired ways. Many researchers are interested in using formal specifications to develop correct systems, relying on the specifications as a means for reasoning about properties of systems and their behaviour. In this thesis we focus on systems whose behaviour is described in a syntax-directed, rule-based fashion. Such systems are typically encoded through a description of the relevant objects of the system along with some relations between these objects defined through a collection of rules. Properties of such systems are expressed through these object relations, relating the validity of certain relations to the validity of others. A specification language based on the dependently typed lambda-calculus, the Edinburgh Logical Framework, or LF, is often used for specifying such systems. The objects of interest in the system are formalized through terms in the specification, and the dependencies permitted in types provide a natural means for formalizing the relationships between objects of the system. Under such an encoding, the terms inhabiting the dependent types of LF represent valid derivations of the relation in the system and thus reasoning about type inhabitation in LF will correspond to reasoning about the validity of relations in the system. This thesis develops a framework for formalizing reasoning about specifications of systems written in LF, with the ultimate goal of formalizing the informal reasoning steps one would take in an LF setting. This formalization will center around the development of a reasoning logic that can express the sorts of properties which arise in reasoning about such specifications. In this logic, type inhabitation judgements in LF serve as atomic formulas, and quantification is permitted over both contexts and terms in these judgements. The logic permits arbitrary relations over derivations of LF judgements to be expressed using a collection of logical connectives, in contrast to other systems for reasoning about LF specifications. Defining a semantics for these formulas raises issues which we must address, such as how to interpret both term and context quantification as well as the relation between atomic formulas and the LF judgements they are meant to encode. This thesis also develops a proof system which captures informal reasoning steps as sound inference rules for the logic. To achieve this we develop a collection of proof rules including mechanisms for both case analysis and inductive reasoning over the derivations of judgements in LF. The proof system also supports applying LF meta-theorems through proof rules that enforce the requirements of the LF meta-theorem that cannot be expressed in the logic. We also implement a proof assistant called Adelfa that provides a means for mechanizing the approach to reasoning about specifications written in LF that is the subject of this thesis. A characteristic of this proof assistant is that it uses the proof rules that complement the logic to describe a collection of tactics that can be used to develop proofs in goal-driven fashion. One of the problems to be solved in this context is that of realizing the rule in the proof system that enables the analysis of LF typing judgements that appear as assumption formulas. We show that a form of unification called higher-order pattern unification can provide the basis for such a realization. The Adelfa system is used to develop a collection of examples which demonstrate the effectiveness of the framework and to showcase how informal reasoning about specifications written in LF can be formalized using the logic and associated proof system.