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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

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

18:00
15m
Talk
A Coq Formalization of Data Provenance
CPP
Véronique Benzaken Université Paris Saclay, Sarah Cohen-Boulakia LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay, Evelyne Contejean CNRS, Chantal Keller LRI, Univ. Paris-Sud, Rébecca Zucchini LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay
Pre-print Media Attached
18:15
15m
Talk
Developing and certifying Datalog optimizations in Coq/MathComp
CPP
Pierre-Léo Bégay Orange Labs & Verimag, Pierre Crégut Orange Labs, Jean-François Monin Verimag
Pre-print Media Attached
18:30
15m
Talk
Machine-Checked Semantic Session TypingDistinguished Paper Award
CPP
Jonas Kastberg Hinrichsen IT University of Copenhagen, Daniël Louwrink University of Amsterdam, Robbert Krebbers Radboud University Nijmegen, Jesper Bengtson IT University of Copenhagen
Pre-print Media Attached