Modalities (temporal, epistemic, deontic, etc) have proved themselves extremely useful in theoretical computer science, multi-agent systems and AI, usually in the setting of classical logic.  Recently there has been a renewed interest in the notions of *constructive* (or intuitionistic) modal type theory and linear type theory, in part because of the interest in homotopy type theory. Since I have been working on modal extensions of the Curry-Howard correspondence to logical systems since the 90s, it seems a good idea to recap some of the old ideas associated with modal type theory. Especially because it seems to me that there are plenty of old problems that have not been solved, yet.

Computing devices are ubiquitous nowadays: they are in your phone, in your car, at home, at work, pretty much everywhere you go. As such, our lives rely on the correct functioning of these computing devices, sometimes in safe-critical ways since they are also found in systems such as medical devices or control systems for airplanes, etc. Making sure that these devices are correctly designed and being able to rely on their expected behaviour is then paramount to us. In this talk, I will describe how logic has allowed us to solve very challenging problems in computer science related to the formal verification and automated design of computer systems by providing mechanisms (a mathematical proof!) that guarantee that a given computer system does indeed satisfy some desirable user-defined properties, e.g., safety properties of many of the systems our lives typically rely upon. This talk will not assume any prior knowledge about logic or computer science, and will slowly take you through the history of logic in computer science, from the Greeks to today’s state of the art in formal verification, and focus on “recent” advances in the last decades in the automated design and verification of computer systems, in particular, those consisting of multiple interacting agents. 

The notion of preference is important in philosophy, decision theory, and many other disciplines. It is the interplay of information and preferences that provides the driving force behind what we actually do. In this tutorial, I will first introduce the structured preference models to account for a richer notion of preference. Then, I will  argue that preference is not static, and it changes dynamically when triggered by various kinds of events. I will illustrate how a wide variety of preference changes can be studied in logic. 

Reference:

Fenrong Liu, Reasoning about Preference Dynamics, Synthese Library 354, Springer 2011

Fenrong Liu, 'Preference change', in S. O. Hansson and V. Hendricks eds., Introduction to Formal Philosophy, pp.549-566, Springer 2018