Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 18:15 - 18:30 at CPP - Semantics Chair(s): Yannick Zakowski

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.

Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:00 - 18:45: SemanticsCPP at CPP
Chair(s): Yannick ZakowskiInria

Streamed session: https://youtu.be/Qak5mK92etU

18:00 - 18:15
Talk
A Coq Formalization of Data Provenance
CPP
Véronique BenzakenUniversité Paris Saclay, Sarah Cohen-BoulakiaLRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay, Evelyne ContejeanCNRS, Chantal KellerLRI, Univ. Paris-Sud, Rébecca ZucchiniLRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay
Pre-print Media Attached
18:15 - 18:30
Talk
Developing and certifying Datalog optimizations in Coq/MathComp
CPP
Pierre-Léo BégayOrange Labs & Verimag, Pierre CrégutOrange Labs, Jean-François MoninVerimag
Pre-print Media Attached
18:30 - 18:45
Talk
Machine-Checked Semantic Session TypingDistinguished Paper Award
CPP
Jonas Kastberg HinrichsenIT University of Copenhagen, Daniël LouwrinkUniversity of Amsterdam, Robbert KrebbersRadboud University Nijmegen, Jesper BengtsonIT University of Copenhagen
Pre-print Media Attached