Towards a Logic for Reasoning About LF Specifications

TL;DR

This paper develops a logic framework for reasoning about LF specifications, enabling formal analysis of typing judgments and contexts with a focus on proof rules and semantics.

Contribution

It introduces a novel logic for LF specifications, including semantics, proof rules, and case analysis, advancing formal reasoning capabilities in LF.

Findings

Defined a logic with atomic formulas as LF typing judgments

Presented semantics and proof rules ensuring normal forms

Illustrated the proof system with an example

Abstract

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.