Stream: Coq users

Topic: Lists and Multisets


view this post on Zulip Adrián García (Aug 23 2021 at 01:42):

My thesis advisor asked me to find the current work about lists and multisets in Coq's library for a bachelor's degree. Is looking at coq.inria.fr/library a good idea to start with or does someone knows an interesting line of research about it? Thanks!

view this post on Zulip Olivier Laurent (Aug 23 2021 at 06:48):

This is a good starting point but alternative developments could also be found in other libraries:
https://github.com/coq/coq/wiki#coq-libraries
https://github.com/coq/stdlib2/wiki/Other-%22standard%22-libraries

view this post on Zulip Olivier Laurent (Aug 23 2021 at 06:55):

Additional work on multisets:
http://color.inria.fr/doc/CoLoR.Util.Multiset.MultisetList.html
https://github.com/coq-contribs/fsets/blob/master/MultiSets.v
https://github.com/meta-logic/coq-ll/blob/master/PLL/LL/Multisets.v
https://github.com/olaure01/ollibs/blob/master/fmsetlist.v

view this post on Zulip Paolo Giarrusso (Aug 26 2021 at 03:43):

I'll inline https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/gmultiset.v even if stdpp is probably reachable from the above links


Last updated: Feb 04 2023 at 20:02 UTC