Foundations Seminar

02/10/2026 Michael Schwarz (National University of Singapore) and Vesal Vojdani (University of Tartu): Thread-Modular Abstract Interpretation with Goblint.

Abstract: Goblint is a framework for mixed flow-sensitive abstract interpretation of multithreaded C. Its analyses are expressed as side-effecting constraint systems. This architecture decouples analysis specifications from generic fixpoint solving, supports modular combinations of flow-sensitive local states and flow-insensitive global invariants, and admits precision refinements through digests and solver update rules.

Vesal Vojdani will present these foundations and connect them to recent work on making analysis results transparent and explorable. Michael Schwarz will show how digests, i.e., computational history abstractions, can be used to exclude spurious thread interactions and improve analysis precision. He will also show how analyses are implemented and composed in Goblint’s OCaml framework. The tutorial targets researchers interested in designing, extending, teaching, or deploying abstract interpreters.

09/10/2026 No Seminar. KASS in Tallinn.

16/10/2026 Niels Voorneveld (Cybernetica): TBA.

30/10/2026 Samuel Steakly (Tallinn University of Technology): TBA.

06/11/2026 Helmut Seidl (TU Munich): TBA.

13/11/2026 Helmut Seidl (TU Munich): TBA.

20/11/2026 No Seminar. NWPT 2026 in Tartu.

25/09/2026 Cheng-Syuan Wan (Tallinn University of Technology): Proof-relevant interpolation for the sequent calculus of bicartesian categories.

Abstract: Craig interpolation is an important metaproperty of logics. It states that if a formula A -> C is provable in a logic L, then there exists a formula B such that both A -> B and B -> C are provable in L, and B uses only propositional variables shared by A and C. It shows that an implication can be factored into two implications satisfying the variable condition. It is natural to consider the factorization for consequence relations (|-), which is called deductive interpolation.

Maehara's method is used to prove deductive interpolation for logics that have a sequent calculus system. The procedure inspects the structure of derivations and produces interpolation triples consisting of the interpolation formula together with corresponding derivations. Čubrić in the 1990s, and later Saurin, noticed that Maehara's method also carries information about derivations: the derivation obtained by composing the two produced derivations is equivalent to the original one modulo an appropriate equivalence relation on derivations. In other words, cut is a left inverse of the interpolation procedure. This property is called proof-relevant interpolation. From the Curry-Howard-Lambek correspondence perspective, Maehara's method is an effective procedure that computes a factorization of a morphism through an object built only from atoms common to its domain and codomain.

In this talk, I will take proof-relevant interpolation as a broader term which is not only about cut being a left inverse of interpolation but in general, several properties that are related to proofs, proof equivalences, and interpolation, including well-definedness of the interpolation procedure and interpolation as a left inverse of cut. The object calculus is the sequent calculus of bicartesian categories. Its sequents have a single formula in both the antecedent and the succedent, which avoids bureaucracy in sequent calculi that have multiset/list as antecedents and allows us to focus on the essence of proof-relevant interpolation. In addition to the main discussion in sequent calculus, I will also discuss the connection between proof-relevant interpolation and Conduché fibrations.

This talk is based on a work in progress with Noam Zeilberger.

04/09/2026 Dominique Unruh (RWTH Aachen): Mimicking EasyCrypt in Lean.

Abstract: I'll describe the development of "Gaudí's Crypt", a framework in Lean for proving cryptographic systems. It attempts to be compatible with the approaches taken in EasyCrypt, in particular, the EasyCrypt module system. (Work in progress: https://dominique-unruh.github.io/gaudis-crypt/)

02/06/2026 Alberto Pardo (Universidad de la República): Agda formalization of a security-preserving translation between While programs.

Abstract: In this work we focus on the preservation of a security property, called non-interference, through program translation. Concretely, we formalize in Agda a program transformation between secure programs, which was introduced by Hunt and Sands in a POPL'06 paper and that converts While programs typable in a flow-sensitive information flow type system into equivalent programs typable in a flow-insensitive information flow type system. A particular aspect of our formalization is that it follows a fully intrinsically-typed approach in which only well-typed (i.e. secure) programs of the object language are represented, ensuring type safety by construction. A benefit of this approach is that, apart from inherently expressing the transformation between programs, the transformation function also stands for an inductive proof of security preservation.

26/05/2026 Mariana Milicich (University of Tartu): General Resource and Effect Grades.

Abstract: In programming, we can find resources that are time-sensitive; their availability depends on the passage of time or whether specific prerequisite events have occurred. This time-sensitivity can be captured with graded modal types and a graded-monadic effect system. From an operational point of view, a stateful, time-aware semantics describes the behaviour of programs while tracking their run times and the temporal resources operating within them, as shown by Danel Ahman and Gašper Žajdela in 2024.

We extend this line of work to include general grades for both effects and resources by parameterizing the system over an arbitrary ordered monoid. This provides a new graded-monadic effect system that captures time-sensitive resources in a broader way. Thus, instead of only considering resources that become available after a certain amount of time (modelled by natural numbers), our system also accommodates resources bound by an expiration time.

In this talk, I will present the extended type system and operational semantics for capturing general resource and effect grades, together with type-safety results.

05/05/2026 Fosco Loregian (Tallinn University of Technology): The fibration of Lyapunov functions.

Abstract: At the heart of topological dynamics lies a foundational result: every continuous endomap f : X → X on a compact metrizable space admits a decomposition into its chain-recurrent component Rec(X,f) and a complementary gradient-like part. This decomposition is classified, in a suitable sense, by a complete Lyapunov function L : X → ℝ, working like a potential of the system; we observe that for fixed X, such functions are the objects of the fibre of a (generalized) fibration over the category of dynamical systems. This is the fibration of the title.

The structure of the space of approximate orbits (on which L induces a partition of Rec(X,f)) is often highly nontrivial. This space, called the Conley quotient of (X,f), encodes subtle dynamical features. By enriching the equivalence classes of the Conley quotient with a "persistent" order structure, one obtains a more refined invariant of the system, called the "emergent order spectrum". This construction too admits an interpretation in terms of fibered categories.

28/04/2026 Teymur Ismikhanov (University of Tartu): Dichotomy for Axiomatising Inclusion Dependencies on K-Databases.

Abstract: A relation consisting of tuples annotated by an element of a monoid K is called a K-relation. A K-database is a collection of K-relations. In this talk, I will present an overview of our recent paper on the entailment of inclusion dependencies over K-databases. We have established that there is a dichotomy regarding the axiomatisation of the entailment of inclusion dependencies. Specifically, if the monoid is weakly absorptive, then the standard axioms of inclusion dependencies are sound and complete for the implication problem. If the monoid is not weakly absorptive, then it is weakly cancellative and the standard axioms together with the weak symmetry axiom are sound and complete for the implication problem. I will also present a novel variant of the chase procedure which we developed for proving the completeness results.

21/04/2026 Meelis Kull (University of Tartu): Uncertainty in Machine Learning: Calibration, Context, and Decisions (part 2).

Continuation of the previous talk.

14/04/2026 Meelis Kull (University of Tartu): Uncertainty in Machine Learning: Calibration, Context, and Decisions (part 1).

Abstract: Uncertainty in machine learning is often reduced to a single confidence value, but this oversimplification masks deeper problems: what should uncertainty represent, when is it trustworthy, and how should it be used in decision-making? In this talk, I will give a selective overview of these topics, relating to our work on probabilistic predictions and uncertainty quantification in machine learning. I will start from proper scoring rules and calibration, and then move to questions that arise once models are deployed: uncertainty under changing contexts, cost uncertainty, and the relation between predictive quality and downstream value. Along the way, I will discuss several recent directions from our group, including improved calibration through training and post-hoc methods, cautious calibration in high-risk settings, and learning evaluation criteria that better reflect the decisions predictions are ultimately used for. The goal is to present a coherent view of uncertainty as part of the foundations of reliable machine learning.

31/03/2026 Bruno Rucy Carneiro Alves De Lima (University of Tartu): Dynamic Recursive Queries (part 3).

Continuation of the previous talk.

24/03/2026 Bruno Rucy Carneiro Alves De Lima (University of Tartu): Dynamic Recursive Queries (part 2).

Continuation of the previous talk.

17/03/2026 Bruno Rucy Carneiro Alves De Lima (University of Tartu): Dynamic Recursive Queries (part 1).

Abstract: In this series of talks we will go over an increasingly relevant computation paradigm, expressive incremental computation. We start by introducing a simple query language, Datalog, and then, with the Database Stream Processing Theory (DBSP) formal language, iteratively build four query engines: batch; streaming; incremental streaming; and dynamic incremental streaming, with the last one ultimately being an interpreter of an incremental query over streams.

10/03/2026 Tähvend Uustalu (TU Munich): Online algorithms with predictions for a square-packing problem.

Abstract: Online algorithms are algorithms which process a sequence of data and have to make decisions based on partial data, without seeing the entire sequence. Generally, one is interested in minimizing the competitive ratio: the worst-case ratio between the value of the objective function achieved by the algorithm and the actual optimal value. In recent years, there has been a lot of interest in augmenting online algorithms with additional predictions about the input sequence. The goal is to design an algorithm that achieves near-optimal competitive ratio when the predictions are accurate, while still retaining an adequate competitive ratio in all cases; the accuracy of the predictions is not known to the algorithm. We give a general overview of the topic and look at one such algorithm.

17/02/2026 Philipp Joram (Tallinn University of Technology): Derivatives for Containers in Univalent Foundations.

Abstract: Containers are a convenient type-theoretic representation of a wide class of inductive data types. Derivatives of containers compute representations of types of "one-hole contexts", useful for implementing tree-traversal algorithms. We know that we can take the derivative of a container whenever it is discrete, i.e. its positions have decidable equality. In a univalent setting, types represent ∞-groupoids, and containers let us model inductive types with interesting symmetries, such as finite multisets. However, Hedberg's Theorem prevents us from taking derivatives of containers whose positions are higher types: types with decidable equality have trivial higher structure. In this talk, I will show how to circumvent this apparent restriction, and extend derivatives to arbitrary, untruncated containers. These derivatives satisfy the expected basic laws with respect to constants, sums, and products. I derive the chain rule, and show that it is in general non-invertible. For traditional (set-valued) containers, the existence of an invertible chain rule is equivalent to a classical principle. If time permits, I will sketch how to derive a rule for derivatives of smallest fixed points from the chain rule, and Characterize its invertibility. More details can be found in the following preprint: https://arxiv.org/abs/2512.17484 All results are formalized in Cubical Agda, and can be browsed interactively online: https://phijor.me/derivatives/

10/02/2026 Bryce Clarke (Tallinn University of Technology): Restriction limits vs. double-categorical limits.

Abstract: Categories with the same objects but different morphisms can have very different properties. For example, limits in the category Set of sets and functions behave quite differently to those in the category Par of sets and partial functions. One way to account for this difference is to equip Par with the structure of a restriction category, and to study instead restriction limits which are much better behaved (Cockett and Lack, 2007). However, another approach is to construct a double category of sets, functions, and partial functions, and to study double-categorical limits in this setting (Grandis and Paré, 1999). In this talk, I will demonstrate the close relationship between these two ways of studying limits of sets and partial functions, and use this case study to explain the connection between restriction limits and double-categorical limits more generally. No prior knowledge of restriction categories or double categories will be assumed.

10/02/2026 Robin Cockett (University of Calgary): The logic of past and future cones: ordered locales.

Abstract: Past and future light cones arise as an important side-effect of the theory of relativity. One can abstract this aspect — the theory of light cones – into what Chris Heunen and Nesta Van Der Schaaf called "ordered locales". The talk will introduce this theory describing, in particular, the "causal order" induced by these cones. The talk will then focus on the theory of trajectories — and their homotopy — arising from ordered locales. Absolutely no knowledge of physics or relativity theory is required!

16/12/2025 Ohad Kammar (University of Edinburgh): Foundations for type-driven probabilistic modelling (part 2).

Continuation of the previous talk.

09/12/2025 Ohad Kammar (University of Edinburgh): Foundations for type-driven probabilistic modelling (part 1).

Abstract: The last few years have seen several breakthroughs in the semantic foundations of probabilistic and statistical modelling. In this tutorial, we will use types to introduce, use, and organise abstractions for probabilistic modelling. In the first 90-minute lecture, we will describe the language informally and its model in discrete probability. In the second 90-minute lecture, we will use the same language but use a model that supports continuous probability using the recently-developed quasi-Borel spaces. The tutorial is accompanied by exercises for self-study, allowing you to develop a working knowledge and hands-on experience after it.

14/10/2025 Matt Earnshaw (University of Tartu): Introduction to multicategories in logic and computer science.

Abstract: Many familiar concepts in logic and computer science share a common structure: they involve "operations" of several inputs, and these "operations" can moreover be combined. Examples include entailments from a list of assumptions together with the cut rule in logic, derivations in context-free grammars, or simply functions and their composition in programming languages. Multicategories are a simple algebraic gadget that capture this pattern, and provide a modular framework for examining shared phenomena and building richer structures. Lambek introduced multicategories in the 1960s following analogies between logic, linear algebra, and the structure of natural language. Despite their prevalence and usefulness, they remain somewhat underutilized and unknown, even to specialists. This talk will introduce multicategories and their applications through accessible examples, demonstrating how they clarify and connect diverse notions, leading to various interesting avenues of active research. No prior familiarity with categorical notions will be assumed.

07/10/2025 Matteo Campanelli (University of Tartu, Offchain Labs): On the Design of Modern Verifiable Databases.

Abstract: When businesses and other organizations store databases in the cloud, they typically trust that the provider will return accurate results. This assumption is problematic—providers may experience undetected faults or, in rare but realistic cases, act maliciously. A verifiable database is a cryptographic protocol that aims to solve this problem: together with a query response, a client will also receive a certificate of its correctness. Since clients rely on outsourcing for scaling, the fundamental challenge is ensuring that verifying this certificate is orders of magnitude cheaper than recomputing the query. In this talk we will discuss principles through which one can design such schemes and the tradeoffs between relying on generic cryptographic tools vs simpler components. This discussion will motivate the choices behind qedb, a recent verifiable database scheme which improves on the state of the art in expressivity, performance, and modularity.

30/09/2025 Acharya Kishor (University of Tartu): An Introduction to Information-Theoretic Measures and their Applications.

Abstract: Since Claude Shannon’s seminal 1948 paper “A Mathematical Theory of Communication”, information has become a quantity that can be rigorously defined and measured, much like energy or mass. This revolutionised communication theory and became fundamental to the digital revolution. Beyond engineering, the information-theoretic perspective—that systems can be described in terms of information storage, transfer, and transformation—has since permeated diverse disciplines including neuroscience, economics and social sciences.In this talk, I will develop an intuitive understanding of key measures such as entropy, mutual information, transfer entropy, and their extensions. I will then discuss how these quantities can be estimated from data, both discrete and continuous, highlighting challenges and available estimation techniques. To bridge theory and practice, I will demonstrate our open-source Python package infomeasure, with examples of how to compute these measures in real datasets. Finally, I will present some of our recent results, including functional network reconstruction and information decomposition in air-transport systems, and point to broader applications of information-theoretic analysis across diverse domains.

23/09/2025 Dominique Unruh (RWTH Aachen): Quantum References.

Abstract: In quantum systems, we often have to refer to a part of a bigger systems (when talking about a "quantum register", "subsystem", or "quantum variable"), especially when we want to talk about quantum algorithms or quantum programming language semantics. But it is not always formally clear what this means (mathematically). Often informal ad-hoc solutions are used. We present (and explain) an approach for solving this problem in a formal way.

19/08/2025 Jens Groth (University College London): Zero-knowledge proofs, zkVMs, and verifiable AI.

Abstract: Verification has always been important, but the scale and rigor is growing with the increasing ability to fake data, humans, and history. Zero-knowledge proofs enable verifiable computation and other ways to verify the correctness of claims. This will be a non-technical big picture talk about the past, present and future of zero-knowledge proofs and their role in verifiability. We start with zero-knowledge proofs and their evolution. Next, we look at zkVMs that make it easy for developers to execute programs with provably correct outputs. Finally, we look into the future of verifiability and its interplay with AI.

10/06/2025 Arnaud Durand (Université Paris Cité): An introduction to algorithms and complexity of counting and enumeration problems.

Abstract: Counting and enumerating are important tasks in algorithms: the former amounts to determine how many solutions has a given instance of a problem while the latter tries to generate one by one every such solutions. If the complexity of counting problems is an old field of theoretical computer science, enumeration has emerged only in the last 15 years in domains such as graphs algorithms and data management. In this talk we will introduce, through examples, some challenging problems in these areas and presents complexity measures which, for the case of enumeration problems, noticeably differs from the usual measures used for decision or optimisation. Examples will be taken in different areas such as graphs and combinatorial algorithms but also query answering in database theory. We will also illustrate how concepts coming from graph and hypergraph decompositions, from Boolean and algebraic circuits complexity are often mobilized to prove lower bound or to design efficient algorithms in these settings.

03/06/2025 Maiara Bollauf (University of Tartu): Smooth (or Not So Smooth) Lattice Sampling.

Abstract: In this talk, we will discuss how to wisely select points from a Gaussian distribution over a lattice, known as Gaussian sampling. This process lies at the heart of many lattice-based cryptographic constructions, particularly in the design of digital signatures schemes that are believed to resist against quantum attacks. We will introduce the mathematical foundations of Gaussian sampling in the context of lattices and review the current techniques together with their strengths, limitations and practical implications. Finally, we will present our contributions to the recent advancements in the field.

27/04/2025 Henrik Wachowitz (LMU Munich): Software Verification in Practice: A look at CPAchecker, DSS and Fm-Weck.

Abstract: In this talk I will present techniques developed at SoSy-Lab that apply the theoretical aspects of software verification in a practical context. I will explain how the CPA algorithm works as a general framework to plug together several verification techniques, how we can use Distributed Summary Synthesis to scale the CPA algorithm and how the tools are made available through infrastructure like Fm-Weck. I will also briefly introduce SV-COMP and highlight the community effort to standardize an exchange format for verification results.

13/04/2025 Roberto Parisella (Simula UiB): Plonk is sound, and your money is safe.

Abstract: Plonk is a popular state-of-the-art zero-knowledge proof scheme used in industrial applications to secure billions of dollars and private data. However, Plonk's original security proof is more a heuristic proof rather than a solid cryptographic proof based on solid mathematical foundations. In this seminar, I will discuss the work done with Helger Lipmaa and Janno Siim over the last two years. We first discovered a bug in Plonk's security proof. In particular, we show an attack on one of the cryptographic primitives (the KZG commitment scheme) used in Plonk, proving that the heuristic used fails to guarantee its security. This left open the question of whether Plonk and other constructions relying on the KZG commitment scheme are actually secure. To answer this question, we first closed a long-standing open problem by proving the security of the KZG commitment scheme (a cryptographic primitive of fundamental importance) on solid mathematical foundations. Finally, we extend the result to prove Plonk's security.

12/04/2025 Robert Tarjan (Princeton University): My life in data structures.

Abstract: Robert Tarjan reflects on over five decades of research in algorithm design and data structures. He will share key milestones, from foundational breakthroughs like union-find and Fibonacci heaps to more recent developments, offering personal insights into the evolving landscape of theoretical computer science. The talk will highlight both the mathematical elegance and practical impact of data structures, weaving together history, technical depth, and anecdotes from a pioneering career.

06/05/2025 Vesal Vojdani and Simmo Saan (University of Tartu): Advanced Software Verification Techniques in Practice.

Abstract: This seminar presents an overview of the state-of-the-art in automated software verification. We will cover foundational methods like abstract interpretation, software model checking, and symbolic execution, referencing their performance in competitions such as SV-COMP. We'll give some examples of how these techniques can be applied to open-source software, and how Airbus and Amazon Web Services use them in practice. To be more concrete, we’ll demonstrate developing a simple static analysis checker using Facebook's Infer framework.

29/04/2025 Ago-Erik Riet (University of Tartu): Distributed data storage, service and computation.

Abstract: The amount of data in the world is growing at an exponential rate. It is important that the data be stored, e.g. in a cloud service such as Google, Amazon, Microsoft clouds, securely, so that its integrity is preserved, it is always available, and updates and computations on the data work well. Typically linear codes with special properties are applied in such distributed storage systems. I will introduce some requirements such a system might need to satisfy. I will introduce regenerating codes, locally repairable codes, codes allowing for efficient data updates, and give some examples. In the second part of the talk I will discuss distributed storage systems with a focus on data recovery, the so-called distributed service systems that need to serve hot data. An example is a system storing newspaper articles where the relative demands for different articles may change. I will introduce the service rate region, classical and asynchronous batch codes, and private information retrieval (PIR) codes. I will talk about a nice fundamental mathematical conjecture about batch codes and discuss its connections with some recent work in combinatorics.

22/04/2025 Vitaly Skachek (University of Tartu): Achieving reliable communications and data storage using error-correcting codes.

Abstract: In this survey talk, we discuss fundamental concepts in coding theory. We start with the Shannon-Weaver communications model and its main components. Then, we discuss error-correcting codes and their main parameters. We present Reed-Solomon codes, and their application to secret-sharing in cryptography. We also discuss low-density parity-check codes. Finally, we discuss some new applications of coding theory in flash memories and in distributed data storage.

08/04/2025 Helger Lipmaa (University of Tartu): On Zero-Knowledge and Zk-SNARKs (part 2).

Continuation of the previous talk.

01/04/2025 Helger Lipmaa (University of Tartu): On Zero-Knowledge and Zk-SNARKs (part 1).

Abstract: Zero-knowledge proofs (ZK), and in particular zk-SNARKs (ZK succinct arguments of knowledge), have become popular in both industry and academia due to their core promise: they allow one to efficiently verify that a computation was done correctly without re-running the entire computation or revealing the prover's private data. Over the past five years, interest in zk-SNARKs has surged, largely thanks to blockchain applications that come with significant funding. Current zk-SNARKs can prove the correctness of arbitrary computations w and structured computations with a factor of overhead 100000 and 10, respectively. Importantly, verification of the correctness of an arbitrary computation usually takes just milliseconds. In the first seminar, I will give a short overview of the state of the art. In the second seminar, I will introduce some example protocols.

18/03/2025 Raul Vicente (University of Tartu): On heads and tails (part 2).

Continuation of the previous talk.

11/03/2025 Raul Vicente (University of Tartu): On heads and tails (part 1).

Abstract: In this talk, I will introduce you to the puzzling geometrical patterns that are formed by some neurons in your brain. In particular, I will talk about grid cells, which are neurons that exhibit striking hexagonal firing patterns that provide a spatial metric for navigation. I will propose that mathematically these patterns can be viewed as eigenfunctions of certain operators that generalize the familiar Fourier transform. Hence, during the talk I will provide evidence that the grid cell phenomenon can be cast as a problem in pattern formation and show how the neural substrate can act as linear (or mildly nonlinear) operator whose eigenfunctions tile the plane with periodic structures. Connections to classical Fourier analysis, spectral geometry, and pattern formation will be highlighted. This talk will be accessible to graduate students in mathematics and researchers interested in the interface of analysis, geometry, and neuroscience. As for the title, it will hopefully make sense by the end of the talk :)

25/02/2025 Dominique Unruh (RWTH Aachen): Quantum crypto and the difficulties of proving it.

Abstract: Quantum cryptography differs from traditional cryptography in that either the adversary or the honest protocol participants use quantum computers or quantum communication. This can lead to many novel possibilities, but it also means that we need to revisit everything: what's possible, what's impossible, how to prove security. Especially on the "how to prove security" side, things tend to get a lot harder. I will give a small intro into quantum computing, explain some difficulties in quantum crypto on the example of zero-knowledge, and in conclusion also tell a bit about how we can formally check quantum security proofs on the computer (Hoare logics etc.).

21/01/2025 Miika Hannula (University of Tartu): Dependence logic (and consistent query answering).

Abstract: Dependence logic extends first-order logic by introducing novel dependence atoms which explicitly assert dependence relations between variables. The aim is to obtain a formal language for modeling and reasoning about phenomena involving complex dependence notions. In general, dependence and independence are concepts that become manifest only in the presence of multitudes. To capture this, dependence logic employs team semantics which evaluates formulas over sets of variable assignments instead of single assignments, as in classical logics. This talk surveys the basic ideas and results in this field, which was introduced in 2007. Time permitting, we will revisit the theme of query evaluation, with a focus on handling uncertainty. Specifically, we will consider consistent query answering, which is a query evaluation paradigm for databases with inconsistent information. Since its inception in 1999, this topic has remained a central research area in the database theory community.

16/12/2024 Miika Hannula (University of Tartu): Query Evaluation: Basics and Recent Developments.

Abstract: Query evaluation is perhaps the most central problem pertaining to databases. Given a query q, a value c, and a database D, this problem is to determine whether or not c belongs to the output q(D) of the query q on the database D. Unfortunately, this problem is NP-complete even if we restrict to conjunctive queries which correspond to the most basic kind of SQL queries. What explains, then, that databases are so successful in practice? In this talk we look how theoretical investigation has helped to tame the query evaluation problem leading to efficient algorithms. We also look into recent developments regarding (a) query evaluation over inconsistent databases, and (b) application of information theory to join queries.