In the domain of knowledge representation and performant reasoning, Datalog engines play an ever-increasingly crucial role. The crux of their operation lies in materialization: the evaluation of a Datalog program and its incorporation into a database. This operation becomes complex and resource-intensive, especially when the data is highly dynamic. Thus, incremental materialization, adjusting the computation to new data instead of restarting it, is the norm. Handling the deletion of data however is significantly more complicated than addition, due to the cascading effects of what is to be removed. In this talk, we dive into the current status of attempting to tame that problem, going from new takes on the ubiquitous delete-rederive algorithm, to lifting Datalog onto other computational models.

Reasoning about socially interacting rational agents is about strategic abilities of individuals (agents) and groups (coalitions) of individuals to guarantee the achievement of their desired objectives, while acting and interacting within an entire society of agents. Several logical systems have been proposed for formalising and capturing such reasoning, starting with the Coalition Logic (CL), the Alternating Time Temporal Logic (ATL) and some extensions of these, introduced the early 2000s.

Coalition Logic provides a natural, but rather restricted perspective: the agents in the proponent coalition are viewed as acting in full cooperation with each other but in complete opposition to all agents outside of the coalition, which are thus treated as adversaries. The Alternating Time Temporal Logic extends Coalition Logic with temporal operators allowing for expressing long-term temporised goals.

The strategic interaction in real life is much more complex, usually involving various patterns combining cooperation and competition. To capture these, more expressive and versatile logical frameworks are needed.

In this talk I will first present briefly Coalition Logic and then will introduce and discuss some more expressive and versatile logical systems, including some of these:

i. the Socially Friendly Coalition Logic (SFCL), enabling formal reasoning about strategic abilities of individuals and groups to ensure achievement of their private goals while allowing for cooperation with the entire society;

ii. the Logic of Coalitional Goal Assignments (LCGA), capturing reasoning about strategic abilities of the entire society to cooperate in order to ensure achievement of the societal goals, while simultaneously protecting the abilities of individuals and groups within the society to achieve their individual and group goals.

iii. the Logic for Conditional Strategic Reasoning ConStR, formalising reasoning about agents’ strategic abilities conditional on the actions that they expect the other agents to take.

In conclusion, I will take a more general perspective on a unifying logic-based framework for strategic reasoning in social context.

In many programming languages, algebraic data types (ADTs) are a flexible tool to implement a variety of complex data structures. Their syntax and semantics are well understood, including the behavior of recursive data types. It is more complicated however to understand symmetries of such types.

We introduce algebraic data types via the framework of containers. We explain how to use containers to build ADTs with interesting symmetries, and show how to write algorithms that respect those symmetries by design.

Modern mathematical logic is known to have developed, albeit with many precursors, in the second half of the nineteenth century. John Cook Wilson, who was the Wykeham Professor of Logic at the University of Oxford from 1889 to his death in 1915, opposed the new logic. As such, he belonged to the group of `leading philosophers, or let us better say the men who occupied the chairs of philosophy', as Hans Reichenbach described them, who did not endorse modern logic. This attitude played a role in shaping Cook Wilson's poor reputation among logicians. Peter Geach even held him to be an `execrably bad logician'. This severe judgement conceals a more complex picture which the present talk aims to unveil.

In the 1920s, von Neumann developed the Hilbert space formulation of quantum mechanics which was later widely adopted as the standard approach to quantum theory. However, in 1935 von Neumann wrote, "I would like to make a confession which may seem immoral: I do not believe absolutely in Hilbert space any more." In the subsequent years he developed a logico-algebraic approach to quantum theory. In this talk, I will review von Neumann and Birkhoff's construction according to which quantum mechanics gives rise to non-classical logic.

Practically speaking, all modern program analysis tools involve solving logical formulas. In this talk my focus is on some key applications that have been developed at Microsoft. I will stay focused on some of those applications, while the overall impact is much broader and often involves academic collaborations and applications outside of Microsoft. A large role in this context is being played by Satisfiability Modulo Theories or SMT---a technology that has been developed around the world, in both industry and academia, at Microsoft in the form of the tool Z3---this technology is itself also continuously evolving, driven by new applications. Other tools often use SMT as a core underlying technology, including tools such as F* and Zen. Other tools have been developed for design, like TLA+. During this talk, I will try to point out applications in the full range from design to diagnoses. The presentation aims at providing a tool-oriented view of the application of logic.

Kurt Gödel (1906-1978) was a secretive character who published very little. His foremost result, the incompleteness theorem, revolutionized the foundations of mathematics in 1931. By 1937, he had come half-way through with the solution of Hilbert's famous first problem about the cardinality of the set of real numbers. After this success, Gödel's only new published results were about the strange circular-time solutions to the field equations of Einstein's theory of general relativity he had found in 1949.

The study of Gödel's tens of thousands of pages of notebooks since 2017, written in an abandoned shorthand, gives a picture of his achievements, as well as of the aims of his life, that is a lot richer than suggested by his publications. As to achievements, there is a plethora of results on logic and foundations of mathematics he revealed to no one. As to the aims, these reflect a vision of science and philosophy he had formed early on in his life, while still a high-school student.