Towards a Logic for Reasoning About LF Specifications

We describe the development of a logic for reasoning about specifications in the Edinburgh Logical Framework (LF). In this logic, typing judgments in LF serve as atomic formulas, and quantification is permitted over contexts and terms that might appear in them. Further, contexts, which constitute ty...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2018-06
Main Authors: Southern, Mary, Nadathur, Gopalan
Format: Article
Language:English
Subjects:
Collection
Judgments
Logic
Reasoning
Semantics
Specifications
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We describe the development of a logic for reasoning about specifications in the Edinburgh Logical Framework (LF). In this logic, typing judgments in LF serve as atomic formulas, and quantification is permitted over contexts and terms that might appear in them. Further, contexts, which constitute type assignments to uniquely named variables that are modeled using the technical device of nominal constants, can be characterized via an inductive description of their structure. We present a semantics for such formulas and then consider the task of proving them. Towards this end, we restrict the collection of formulas we consider so as to ensure that they have normal forms upon which proof rules may be based. We then specifically discuss a proof rule that provides the basis for case analysis over LF typing judgments; this rule is the most complex and innovative one in the collection. We illustrate the proof system through an example. Finally, we discuss ongoing work and we relate our project to existing systems that have a similar goal.
ISSN:2331-8422