Adelfa: A system for reasoning about LF specifications

Mary Southern, Gopalan Nadathur

Research output: Contribution to journalConference articlepeer-review

Abstract

We present a system called Adelfa that provides mechanized support for reasoning about specifications developed in the Edinburgh Logical Framework or LF. Underlying Adelfa is a new logic named LLF. Typing judgements in LF are represented by atomic formulas in LLF and quantification is permitted over contexts and terms that appear in such formulas. Contexts, which constitute type assignments to uniquely named variables that are modelled using the technical device of nominal constants, are characterized in LLF by context schemas that describe their inductive structure. We present these formulas and an associated semantics before sketching a proof system for constructing arguments that are sound with respect to the semantics. We then outline the realization of this proof system in Adelfa and illustrate its use through a few example proof developments. We conclude the paper by relating Adelfa to existing systems for reasoning about LF specifications.

Original languageEnglish (US)
Pages (from-to)104-120
Number of pages17
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume337
DOIs
StatePublished - Jul 16 2021
Event16th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021 - Pittsburgh, United States
Duration: Jul 16 2021 → …

Bibliographical note

Funding Information:
This paper is based upon work supported by the National Science Foundation under Grant No. CCF-1617771. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.

Publisher Copyright:
© 2021 M. Southern & G. Nadathur.

Fingerprint

Dive into the research topics of 'Adelfa: A system for reasoning about LF specifications'. Together they form a unique fingerprint.

Cite this