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.

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

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.

append contains an HH specification for the append relation between polymorphic lists.
append contains the proofs and applications of its determinacy property.

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:

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.

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.

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.

A compiler verification project that exploits schematic polymorphism

See Verified Compilation of Functional Programs .

We have developed a compiler for an extension of PCF using the original Abella without support of polymorphism. The development can be found at here.
Later we ported the whole development to Abella with schematic polymorphism. The development can be found at here.

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.

Acknowledgements

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.