3 ms·
HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics
- bsaul 8y agois there any project that sould convert coq proofs into another language than ML, even if that means making a few assumptions or using only a subset of the target language ?