Bas Spitters
Bas Spitters
@denismerigoux is working on a concrete equivalence proof in F*, so he may have insights on how to structure this.
@burdges could elaborate on how this differs from persistent data structures? The concepts seems similar.
https://github.com/mit-plv/fiat-crypto allows one to generate efficient rust code directly. @huitseeker will also be interested.
Interesting. Are these changes so big that this cannot be reintroduced in the future? Fiat provides quite a big suite of primitives and curves.
We (=@RasmusHoldsbjergCSAU) are working on the in Aarhus :-) Still work in progress... https://github.com/RasmusHoldsbjergCSAU/QuadraticFieldExtensions/tree/master/LazyReduction
With #105 merged, what is the status of this? What would still need to be done?
The coq-community uses zenodo for citations to github, if we want to follow that lead. For bibliometrics/analysis it's probably clearer if people cite the paper.
https://github.com/coq-community/manifesto/issues/75 On Sun, Jul 5, 2020 at 3:26 PM Mike Shulman wrote: > What would it mean to "use zenodo"? > > — > You are receiving this because you...
Authors could be "HoTT library team", following "Coq Team"...
I'm not sure there is a perfect solution. For e.g. agda people still cite Ulf's PhD thesis. Citations to GAP, and even the HoTT book don't get picked up by...