Document Type

Technical Report

Department

Computer Science and Engineering

Publication Date

2008-01-01

Filename

wucse-2008-7.pdf

DOI:

10.7936/K79K48G0

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

Download

Share

COinS