A Logic for Formalizing Properties of LF Specifications
Gopalan Nadathur, Mary Southern · 2022
A logic is presented for formalizing properties of specifications in the Edinburgh Logical Framework or LF. In this logic, typing judgments in LF serve as atomic formulas and quantification is permitted over LF terms and contexts. Quantifiers of the first variety are qualified by simple types that describe the functional structure associated with the variables they bind. Quantifiers over contexts are typed by context schemas that constrain their instantiations to adhere to a regular structure. The semantics of the logic is based ultimately on an understanding of derivability in LF. As such, valid formulas in the logic represent meta-theoretic properties of object systems that are encoded via LF signatures. The logic is complemented by a proof system that is briefly discussed. There are two categories to the rules in this proof system. One collection of rules captures the meanings of logical connectives and quantifiers. Another collection provides a means for analyzing atomic formulas based on an understanding of derivability in LF; these rules build in the capability for a case-analysis style reasoning about LF judgements and for induction over the heights of LF derivations.