Schematic polymorphism in the Abella proof assistant

Gopalan Nadathur, Yuting Wang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The Abella interactive theorem prover has turned out to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic: formalizations that are identical except in the respect that they apply to different types have to be repeated at each type. We develop an approach that overcomes this limitation while preserving the logical underpinnings of the system. In this approach object constructors, formulas and other relevant logical notions are allowed to be parameterized by types, with the interpretation that they stand for the (infinite) collection of corresponding constructs that are obtained by instantiating the type parameters. The proof structures that we consider for formulas that are schematized in this fashion are limited to ones whose type instances are valid proofs in the simply typed logic. We develop schematic proof rules that ensure this property, a task that is complicated by the fact that type information influences the notion of unification that plays a key role in the logic. Our ideas, which have been implemented in an updated version of the system, accommodate schematic polymorphism with respect to the logic that Abella is based on as well as the executable specification logic that it embeds.

Original languageEnglish (US)
Title of host publicationProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018
PublisherAssociation for Computing Machinery
ISBN (Electronic)9781450364416
DOIs
StatePublished - Sep 3 2018
Event20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018 - Frankfurt am Main, Germany
Duration: Sep 3 2018Sep 5 2018

Publication series

NameACM International Conference Proceeding Series

Other

Other20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018
CountryGermany
CityFrankfurt am Main
Period9/3/189/5/18

Bibliographical note

Funding Information:
This work has been supported by the National Science Foundation grants CCF-1617771, 1521523 and 1715154 and DARPA grants FA8750-12-2-0293, FA8750-16-2-0274, and FA8750-15-C-0082. The U.S. Government is authorized to reproduce and distribute reprints for governmental purposes notwithstanding any copyright notation thereon. Opinions, findings and conclusions or recommendations that are manifest in this material are those of the participants and should not be interpreted as necessarily representing the official policies or to have the endorsements, either expressed or implied, of NSF, DARPA or the U.S. Government.

Fingerprint Dive into the research topics of 'Schematic polymorphism in the Abella proof assistant'. Together they form a unique fingerprint.

Cite this