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.

- rappend contains the fixed-point definition of the append relation for polymorphic lists and the proofs and applications of its determinacy property.

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:

- schm_fail contains some examples showing that schematic proofs do not always exist. In those cases, Abella will stuck at the points the schematic proof rules are not applicable.

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.

- subst contains an encoding of substitutions as relations using schematic polymorphism. It also contains the proofs of some common properties of substitutions, such as their determinacy and stability under instantiation.

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.

The views and opinions expressed in this page are strictly those of the page author(s). The contents of this page have not been reviewed or approved by the University of Minnesota.