Bas Spitters

@mattam82 I understand that these pimitives have been disabled again? @joom any updates on https://github.com/CertiCoq/VeriFFI ?

@vrahli your development is taking a long time. By moving to the community, more people can help fixing that. https://coq-bench.github.io/clean/Linux-x86_64-4.03.0-2.0.5/released/8.6/intuitionistic-nuprl/8.6.0.html

This initiative may be worth mentioning, and being expanded on: https://popl20.sigplan.org/details/CoqPL-2020-papers/2/The-use-of-Coq-for-Common-Criteria-Evaluations On Tue, Jan 28, 2020 at 8:59 PM Karl Palmskog wrote: > Many Coq-community members regularly do advocacy for...

Interesting. Perhaps you can expand the readme a bit. Is there a connected paper? The coq-tools directory seems like material that perhaps should be moved to a more central place.

@strub with ALEA now available in 8.11, would it be a good idea to move certicrypt to the community for posterity ?

In https://github.com/HoTT/HoTT/wiki we collect a bunch of things that are generated automatically using travis: documentation, graphs, proviola code, ... If people like it, I hope it's not too hard to...

Carst has left academia. He did a postdoc with @gares before. I think it could be good to include it in coq-community.

We've been working on a tool-chain for Curve operations using bedrock: https://github.com/AU-COBRA/AUCurves

How about this one? https://github.com/hacspec/hacspec/blob/master/utils/secret-integers/src/lib.rs#L231

It appears that this was not spotted by the CI because it is not included in https://github.com/CertiCoq/certicoq/blob/master/theories/_CoqProject