Deciding Joinability Modulo Ground Equations In Operational Type Theory

Authors

Adam Petcher, Washington University in St Louis
Aaron Stump, Washington University in St Louis

Document Type

Technical Report

Department

Computer Science and Engineering

Publication Date

2008-01-01

Filename

wucse-2008-7.pdf

Technical Report Number

WUCSE-2008-7

Abstract

Operational Type Theory (OpTT) can be used to construct and check proofs related to programs, but the development of these proofs can be somewhat tedious. An algorithm is presented that can be used to automatically generate proofs of equality in OpTT. The algorithm takes as input a set of ground equations and two terms that should be tested for joinability modulo the supplied ground equations. The algorithm will equate the terms if and only if there exists an OpTT proof that can equate the two terms using only the proof rules related to evaluation under the operational semantics, symmetry, transitivity, and congruence with respect to the supplied ground equations. The description of this algorithm is accompanied by a proof that the algorithm is partially correct.

Comments

Permanent URL: http://dx.doi.org/10.7936/K79K48G0

Recommended Citation

Petcher, Adam and Stump, Aaron, "Deciding Joinability Modulo Ground Equations In Operational Type Theory" Report Number: WUCSE-2008-7 (2008). All Computer Science and Engineering Research.
https://openscholarship.wustl.edu/cse_research/238