Between Dec 19, 2024 and Jan 2, 2025, datasets can be submitted to DRUM but will not be processed until after the break. Staff will not be available to answer email during this period, and will not be able to provide DOIs until after Jan 2. If you are in need of a DOI during this period, consider Dryad or OpenICPSR. Submission responses to the UDC may also be delayed during this time.
 

A Framework for Reasoning About LF Specifications

Loading...
Thumbnail Image

Persistent link to this item

Statistics
View Statistics

Journal Title

Journal ISSN

Volume Title

Title

A Framework for Reasoning About LF Specifications

Published Date

2021-05

Publisher

Type

Thesis or Dissertation

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.

Description

University of Minnesota Ph.D. dissertation. May 2021. Major: Computer Science. Advisor: Gopalan Nadathur. 1 computer file (PDF); vi, 180 pages.

Related to

Replaces

License

Collections

Series/Report Number

Funding information

Isbn identifier

Doi identifier

Previously Published Citation

Other identifiers

Suggested citation

Southern, Mary. (2021). A Framework for Reasoning About LF Specifications. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/223120.

Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.