2 search results - page 1 / 1 » Information Retrieval in a Coq Proof Library Using Type Isom... |
TYPES
1999
Springer
13 years 9 months ago
1999
Springer
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 funct...
CADE
2005
Springer
14 years 5 months ago
2005
Springer
Our general goal is to provide better automation in interactive proof assistants such as Coq. We present an interpreter of proof traces in first-order multi-sorted logic with equal...