Welcome to the webpage of the logic group at the University of Gothenburg. Information about our research and activities can be found through the links to the left. More detailed information is available through the personal pages of group members and our homepage at the University of Gothenburg.

Past talks can be found on the seminar page. Links to forthcoming talks are distributed via the seminar mailing list.

Dominik Wehr
(FLoV)
– Abstract Cyclic Proofs

Cyclic proof systems permit derivations to contain cycles, thereby serving as finite representations of non-wellfounded derivation trees. Such cyclic proof systems have been proposed for a broad range of logics, especially those with fixed-point features or inductively defined objects of reasoning. The soundness of such systems is commonly ensured by only considering those cyclic derivations as proofs which satisfy a so-called global trace condition.

Nordic Online Logic Seminar

Lars Birkedal
(Aarhus University)
– Iris: A Higher-Order Concurrent Separation Logic Framework
I will introduce some of our research on Iris, a higher-order concurrent separation logic framework, implemented and verified in the Coq proof assistant, which can be used for mathematical reasoning about safety and correctness of concurrent higher-order imperative programs. Iris has been used for many different applications; see iris-project.org for a list of research papers. However, in this talk I will focus on the Iris base logic (and its semantics) and sketch how one may define useful program logics on top of the base logic. The base logic is a higher-order intuitionistic modal logic, which, in particular, supports the definition of recursive predicates and whose type of propositions is itself recursively defined.

This talk is part of the Nordic Online Logic Seminar.