Proof Reuse with Extended Inductive Types

Abstract

Proof assistants based on type theory such as COQ or LEGO, put emphasis on inductive specifications and proofs by featuring expressive inductive types. It is frequent to modify an existing specification or proof by adding or modifying constructors in inductive types. In the context of language design, adding constructors is a common practice to make progress step-by-step. In this article, we propose a mechanism to extend and parameter inductive types, and a proof reuse mechanism founded on proof terms reuse. © Springer-Verlag 2004.