The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

I'm currently using UPenn's metatheory library:

https://github.com/plclub/metalib

I personally know a few people who use this with some success, and
have seen it followed in various papers.  It's not perfect, and I'm
working on some extensions that make dependently typed programming
better (which aren't quite finished yet!) but theirs is a very good
development.  Their paper "Engineering formal metatheory" explains the
problems of dealing with binders in various ways (e.g., PHOAS,
cofinite quantification, etc...).

In particular, their AssocList implementation is very helpful.  I use
this along with a bit of automation, including Adam Chlipala's crush
tactic, and get them to play together.

Kris


On Fri, Aug 2, 2013 at 11:49 AM, Kevin Sullivan
<sullivan.kevinj AT gmail.com>
 wrote:
> Dear Coq Club:
>
> A student and I need to write Coq code using simple finite sets and maps
> (e.g., to build symbol tables, do lookups in 1-n relations, and that sort of
> thing). Types are known statically. Are we best advised to use Coq's FSets
> library, Stéphane Lescuyer's First-Class Containers in Coq, or perhaps
> something else that we don't know about yet?
>
> Kind regards,
> Kevin
>