What are some of the favorite examples of extraction? Some of the ones mentioned at the bottom here are a bit dated.
CompCert. To a lesser extent, Flocq (which is used by CompCert but also by some other compilers or static analyzers).
Hey, we have an example where we use Coq to do partial evaluation and fusion, then extract the code to something quite efficient! https://github.com/draperlaboratory/parts It's a fun application: you really need to be able to evaluate on open terms.
Last updated: Dec 01 2023 at 06:01 UTC