Integrating an Equality Prover into a Software Development System Based on Type Theory

摘要

This paper reports on the integration of an untyped equational prover into a proof system based on an expressive constructive type theory. The proofs returned by the equational prover are effectively verified for type correctness, a proof term can be constructed. The scheme of proof translation described here is illustrated by the integration of the Discount prover into the software development system Typelab.