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

Crit-bit trees #387

Closed vfukala closed 11 months ago

vfukala commented 11 months ago

Adding a verified implementation (lookup and insert) of crit-bit trees as an example in Live Verification.