This page provides supplementary materials for the paper "Schematic Polymorphism in the Abella Proof Assistant".
To run the following proof scripts, you need to download Abella with support of schematic polymorphism. Following the instructions in the README file to install Abella. Make sure the executable is in your search path.
We first present the formal development of examples that use limited features of Abella to prove properties about polymorphic specifications. These are examples from Section 3,4 and 5 in the accompanying paper. Already they are sufficient for demonstrating the core ideas behind schematic polymorphism, including parameterization of definition blocks over types, parameterization of individual clauses in a definition block which enables encoding and reasoning about polymorphic specifications in a specification logic, and type-generic ways to perform case analysis on schematic clauses.
A definition block can be parameterized over types such that each type instance that we generate of it is a valid definition block in the core Abella and is independent of other instances of the block. We show how to construct schematic proofs for properties of such definitions blocks.
Schematization of individual clauses in a definition block is also allowed. This enables us to encode the logic of Hereditary Harrop formulas (HH) as a fixed-point definition in Abella and prove properties about polymorphic HH specifications in Abella.
It is not always possible to construct schematic proofs using the schematic proof rules we designed in the paper and implemented in Abella. The following examples demonstrate this point:
Abella supports a higher-order abstract syntax approach to encoding and reasoning. Combined with schematic polymorphism extension we are able to give a general treatment to many meta-properties of λ-calculus.
See Verified Compilation of Functional Programs .
This material is based upon work supported by the National Science Foundation under Grant No CCF-0917140 and Grant No. CCF-1617771. The work has also received support from the University of Minnesota through a Doctoral Dissertation Fellowship and a Grant-in-Aid of Research. Any opinions, findings and conclusions or recommendations expressed in this material are those of the participants and do not necessarily reflect the views of the National Science Foundation.