Schematic Polymorphism in the Abella Proof Assistant

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.

Simple examples for demonstrating schematic polymorphism in Abella

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.

Parameterization of definition blocks over types

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.

Reasoning about HH specifications

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.

Cases when schematic proofs are not available

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:

A general definition of substitutions as relations using schematic polymorphism

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.

A compiler verification project that exploits schematic polymorphism

See Verified Compilation of Functional Programs .

Using schematic polymorphism has led to a reduction of 14.2%, measured in terms of the lines of code (844 vs. 984), in the formalization of the library components (subst.thm and util.thm) of the latter project in comparison with the former.


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.