A Logic for Formalizing Properties of LF Specifications

Gopalan Nadathur; Mary Southern

doi:10.1145/3551357.3551377

A Logic for Formalizing Properties of LF Specifications

Gopalan Nadathur, Mary Southern

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English (US)
Title of host publication	Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022 - Co-located with CLAS 2022 (including LOPSTR 2022)
Publisher	Association for Computing Machinery
ISBN (Electronic)	9781450397032
DOIs	https://doi.org/10.1145/3551357.3551377
State	Published - Sep 20 2022
Event	24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022 - Virtual, Online, Georgia Duration: Sep 20 2022 → Sep 22 2022

Publication series

Name	ACM International Conference Proceeding Series

Conference

Conference	24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022
Country/Territory	Georgia
City	Virtual, Online
Period	9/20/22 → 9/22/22

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. This work was completed prior to Mary Southern’s joining Amazon.

Publisher Copyright:
© 2022 ACM.

Keywords

case analysis
dependently typed lambda calculi
formalizing and mechanizing reasoning about typing judgements
induction
two-level logic style of reasoning

Access

10.1145/3551357.3551377

OpenUrl availability

Full text

Cite this

Nadathur, G., & Southern, M. (2022). A Logic for Formalizing Properties of LF Specifications. In Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022 - Co-located with CLAS 2022 (including LOPSTR 2022) Article 3551377 (ACM International Conference Proceeding Series). Association for Computing Machinery. https://doi.org/10.1145/3551357.3551377

A Logic for Formalizing Properties of LF Specifications. / Nadathur, Gopalan; Southern, Mary.
Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022 - Co-located with CLAS 2022 (including LOPSTR 2022). Association for Computing Machinery, 2022. 3551377 (ACM International Conference Proceeding Series).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Nadathur, G & Southern, M 2022, A Logic for Formalizing Properties of LF Specifications. in Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022 - Co-located with CLAS 2022 (including LOPSTR 2022)., 3551377, ACM International Conference Proceeding Series, Association for Computing Machinery, 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022, Virtual, Online, Georgia, 9/20/22. https://doi.org/10.1145/3551357.3551377

Nadathur G, Southern M. A Logic for Formalizing Properties of LF Specifications. In Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022 - Co-located with CLAS 2022 (including LOPSTR 2022). Association for Computing Machinery. 2022. 3551377. (ACM International Conference Proceeding Series). doi: 10.1145/3551357.3551377

@inproceedings{9d64c5f7b6084688b48fc759c5da9c72,

title = "A Logic for Formalizing Properties of LF Specifications",

abstract = "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.",

keywords = "case analysis, dependently typed lambda calculi, formalizing and mechanizing reasoning about typing judgements, induction, two-level logic style of reasoning",

author = "Gopalan Nadathur and Mary Southern",

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. This work was completed prior to Mary Southern{\textquoteright}s joining Amazon. Publisher Copyright: {\textcopyright} 2022 ACM.; 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022 ; Conference date: 20-09-2022 Through 22-09-2022",

year = "2022",

month = sep,

day = "20",

doi = "10.1145/3551357.3551377",

language = "English (US)",

series = "ACM International Conference Proceeding Series",

publisher = "Association for Computing Machinery",

booktitle = "Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022 - Co-located with CLAS 2022 (including LOPSTR 2022)",

}

TY - GEN

T1 - A Logic for Formalizing Properties of LF Specifications

AU - Nadathur, Gopalan

AU - Southern, Mary

N1 - 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. This work was completed prior to Mary Southern’s joining Amazon. Publisher Copyright: © 2022 ACM.

PY - 2022/9/20

Y1 - 2022/9/20

N2 - 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.

AB - 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.

KW - case analysis

KW - dependently typed lambda calculi

KW - formalizing and mechanizing reasoning about typing judgements

KW - induction

KW - two-level logic style of reasoning

UR - http://www.scopus.com/inward/record.url?scp=85139593318&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85139593318&partnerID=8YFLogxK

U2 - 10.1145/3551357.3551377

DO - 10.1145/3551357.3551377

M3 - Conference contribution

AN - SCOPUS:85139593318

T3 - ACM International Conference Proceeding Series

BT - Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022 - Co-located with CLAS 2022 (including LOPSTR 2022)

PB - Association for Computing Machinery

T2 - 24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022

Y2 - 20 September 2022 through 22 September 2022

ER -

A Logic for Formalizing Properties of LF Specifications

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this