Stream: Miscellaneous

Topic: Extraction examples

view this post on Zulip Bas Spitters (Feb 09 2021 at 17:49):

What are some of the favorite examples of extraction? Some of the ones mentioned at the bottom here are a bit dated.

view this post on Zulip Guillaume Melquiond (Feb 09 2021 at 19:27):

CompCert. To a lesser extent, Flocq (which is used by CompCert but also by some other compilers or static analyzers).

view this post on Zulip Cody Roux (Feb 10 2021 at 04:07):

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: Oct 08 2024 at 14:01 UTC