Developing and certifying Datalog optimizations in coq/mathcomp. - Pierre-Léo Bégay; Pierre Crégut; Jean-François Monin (CPP, 2021)

Developing and certifying in Coq/MathComp of Datalog optimizations for network verification. (Développement et certification en Coq/MathComp d'optimisations Datalog pour la vérification réseau). - Pierre-Léo Bégay (2021)