Information Retrieval in a Coq Proof Library Using Type Isomorphisms

We propose a method to search for a lemma in a goq proof library by using the lemma type as a key. The method is based on the concept of type isomorphism developed within the functional programming framework. We introduce a theory which is a generalization of the axiomatization for the simply typed λ-calculus (associated with Closed Cartesian Categories) to an Extended Calculus of Constructions with a more Extensional conversion rule. We show a soundness theorem for this theory but we notice that it is not contextual and requires "ad hoc" contextual rules. Thus, we see how we must adapt this theory for goq and we dene an approximation of the contextual part of this theory, which is implemented in a decision procedure.

• Type: Conference
• Year: 1999
• Where: TYPES
• Authors: David Delahaye
• Keywords: Formal Methods, Functional Programming Framework, Goq Proof Library, Lemma Type, TYPES 1999