Generically Automating Separation Logic by Functors, Homomorphisms and Modules

Qiyuan Xu, David Sanan, Zhe Hou +3

Foundational verification considers the functional correctness of programming languages with formalized semantics and uses proof assistants (e.g., Coq, Isabelle) to certify proofs.…