We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: A Framework for Reasoning About LF Specifications

Authors: Mary Southern
Abstract: This thesis develops a framework for formalizing reasoning about specifications of systems written in LF. This formalization centers 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 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 this approach to reasoning about specifications written in LF. A characteristic of this proof assistant is that it uses the proof rules that complement the logic to describe a collection of tactics that are used to develop proofs in goal-driven fashion. The Adelfa system is used to develop a collection of examples which demonstrate the effectiveness of the framework and showcase how informal reasoning about specifications written in LF can be formalized using the logic and associated proof system.
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2105.04110 [cs.LO]
  (or arXiv:2105.04110v1 [cs.LO] for this version)

Submission history

From: Mary Southern [view email]
[v1] Mon, 10 May 2021 04:53:39 GMT (128kb)

Link back to: arXiv, form interface, contact.