Agenda

Département
Langue
Date
Thématique
2026

May

June

  • 11:00
    12:00

    Who does what pt.2

    (not for LaBRI agenda)

    https://algodist.labri.fr/index.php/Main/GT

    English
    LaBRI 178
  • 13:30
    14:30

    Title: Will My Favorite Chases Terminate if Evaluating Conjunctive Queries Does? One Does Not Simply Decide This

    Abstract: Existential rules are a prominent formalism to enrich a database with knowledge from the domain of interest, but make even basic reasoning tasks on the resulting knowledge base undecidable. To circumvent this, several classes of rules offering various useful properties have been identified. One such class, for instance, contains all sets of rules on which the chase algorithm always terminates, which guarantees the existence of a finite universal model. However, these classes are often abstract rather than concrete: it may be undecidable to check whether a given set of rules belongs to them. Given that the most studied classes of existential rules are designed for reasoning on databases, thus ensuring decidable conjunctive query entailment, we ask: Within a class that supports decidable query entailment, do the usual abstract classes become concrete? We answer in the negative for classes based upon the termination of all classical chase variants and for the bts class.

    English
    LaBRI
  • 14:00
    15:00

    Software development is an inherently incremental process. To this end, most programming languages provide basic mechanisms for programmers to indicate that a given functionality is not yet implemented, for instance through dedicated exceptions. Unfortunately, apart from incremental typecheckers, most of the tools used to reason about program correctness—like testing, analysis, and verification frameworks—fail to account for these incompleteness idioms. As a result, programmers are faced with either spurious failure reports or the burden of altering their specifications, which sacrifices the direct causal connection between the code and the reasoning tools. In this talk, I will illustrate this issue in the context of testing, considering both unit testing and property-based testing, as well as certified programming in proof assistants. Examining the problem in such disparate settings allows us to isolate the core concepts required to build truly incremental reasoning tools.

    Bio:
    Éric Tanter is a Full Professor in the Computer Science Department of the University of Chile. He received his PhD from both the University of Nantes and the University of Chile in 2004. His research interests cover programming languages and software engineering, ranging from the theoretical underpinnings of programming languages to the empirical study of the practice of programming. Recently, he has been deeply involved in the foundations and practice of gradual typing and verification. He holds an Inria International Chair for the period 2025-2029. 

    Salle 178 (LaBRI)
  • 12:00
    15:00
    English
    LaBRI