search

mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

coqutil: coinductive version of always #408

Closed andres-erbsen closed 7 months ago

andres-erbsen commented 7 months ago

please fast-forward for fiat-crypto