The Coq mailing list

["Sunil Kothari" <skothari AT uwyo.edu>]

Title: RE: Issues regarding use of finite map interface (FMapInterface)

Many thanks to Stéphane Lescuyer, Brian Aydemir and  Pierre Casteran for your reply to my queries.
Greatly appreciate your inputs.

Sunil

-----Original Message-----
From: Sunil Kothari
Sent: Sun 9/14/2008 11:07 AM
To: coq-club AT pauillac.inria.fr
Cc: Sunil Kothari
Subject: Issues regarding use of  finite map interface (FMapInterface)

Dear Coq users,
   I want to use finite maps in my formalization. I have looked at the various implementations of finite maps available in the CoQ library. However,
 I don't want to restrict my code to any particular implementation. I have a few queries:

  1. In programming languages, we are taught to program against an interface and not to an implementation. Can I formalize by programming against the finite map interface ?  Is there anything wrong in doing so ?

  2. I tried to import the finite map interface  but none of the interface definitions are available in the CoqIde. However, if I import a particular implementation, all the definitions (in that particular implementation) are visible in the CoqIde. Is that intentional ?

 3. Are there formalizations showing usage of any of the implementations of finite maps ? If so, I will appreciate pointers.

 4. Is there literature on the theory behind finite maps as implemented in Coq libraries ? Is it similar to the following paper (HOL implementation) by Don Syme and Graham Collins (available at http://research.microsoft.com/research/pubs/view.aspx?type=Publication&id=595)?

Thanks in advance,
 Sunil