The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here are a few (though I'm not sure you'd call homotopy type theory "practical"):

the HoTT library: https://github.com/HoTT/HoTT

the unimath library: https://github.com/UniMath/UniMath

x86proved, a formalization of x86 assembly (http://x86proved.codeplex.com/)

Bedrock, a Coq library for verified low-level programming (http://plv.csail.mit.edu/bedrock/)

CompCert (http://compcert.inria.fr/)

ssreflect (ssr.msr-inria.inria.fr)

You might find the listing at GitHub's search for repos in Coq useful (sorted by recently updated), and feel free to add any category theory repositories you find to the list of formalizations of category theory I've made on mathoverflow.

-Jason

On Tue, Jul 22, 2014 at 10:37 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

Hi all,

I learned a lot from contributing to open source compilers in the past. I'd like to do same thing to some Coq projects to learn more about practical use of Coq.

I searched in Github to find some projects but couldn't find anything other than 1) not actively developed projects 2) personal repos to keep solved exercises.

At this point I don't have any ideas about what kind of projects to look. A compiler verification project and some kind of algebra formalization project may be very different from each other, but at this point I'm open to all kinds of projects because I don't have any ideas about any of them.

Thanks.

---
Ömer Sinan Ağacan
http://osa1.net