Coq formalisation and mechanisation of privacy aware data integration

Quoting [2]: “Modern hardware and software are monstrously complex. The best tool for coping with this complexity is abstraction—i.e., breaking up functionality into components or layers, with interfaces that are as narrow and clear as possible. Each interface is accompanied—implicitly or explicitly—by a specification expressing the contract between providers and consumers of that interface. These specifications come in a multitude of different forms: comments in code and natural-language documentation, unit tests, assertions, contracts, static types, property-based random test suites, and formal specifications in various logics. Sadly, despite widespread agreement on the importance of abstraction, specifications are often seen as an afterthought, or even a hindrance, to system development. Why? Experience has shown that it is extremely challenging to write good ones. Indeed, a maximally useful interface specification must be simultaneously rich (describing complex component behaviors in detail); two-sided (connected to both implementations and clients); formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs); and live (connected via machine-checkable proofs to the implementation and client code). Specifications with all of these properties are called deep specifications.” Obtaining such specifications requires the use of formal methods and mature tools. A very promising approach consists in using proof assistants such as Isabelle [9] or Coq [8]. In addition, and regardless to deep-specification efforts pursued by the formal methods community, current data management applications and systems have amazingly escaped to this unprecedented, world-wide effort. This is surpring as with the advent of Big data such systems and data engines store and manage and integrate increasingly massive data volumes. The Datacert project aims at providing deep-specification of privacy aware data integration. This intern is settled in this context1.