Developing and certifying Datalog optimizations in Coq/MathComp

Pierre-Léo Bégay1,2 , Pierre Crégut1, and Jean-François Monin2

1 Orange Labs
2 Verimag
Abstract. We introduce a static analysis and two program transformations for Datalog to circumvent performance issues that arise with the implementation of primitive predicates, notably in the framework of a large scale telecommunication application. To this effect, we introduce a new trace semantics for Datalog with a verified mechanization. This work can be seen as both a first step and a proof of concept for the creation of a full-blown library of verified Datalog optimizations, on top of an existing Coq/MathComp formalization of Datalog towards the development of a realistic environment for certified data-centric applications The requirements for compiling the sources are: 
opam list

# Name                 # Installed       # Synopsis
coq                    8.9.1             Formal proof management system
coq-equations          1.2.1+8.9         A function definition package for Coq
coq-mathcomp-finmap    1.4.0       	 Finite sets, finite maps, finitely supported 
coq-mathcomp-ssreflect 1.8.0             Small Scale Reflection