Nordic Online Logic Seminar: next talk on December 20, by Lars Birkedal

[Graham Leigh]

The Nordic Online Logic Seminar (NOL Seminar) is organised monthly over Zoom, with expository talks on topics of interest for the broader logic community. The seminar is open for professional or aspiring logicians and logic aficionados worldwide.

See the announcement for the next talk below. If you wish to receive the Zoom ID and password for it, as well as further announcements, please subscribe here: https://listserv.gu.se/sympa/subscribe/nordiclogic .

Val Goranko and Graham Leigh
NOL seminar organisers

--------------------------------------
Nordic Online Logic Seminar

Next talk: Monday, December 20, 16.00-17.30 CET (UTC+1), on Zoom (details are provided to the subscribers)

Title: Iris: A Higher-Order Concurrent Separation Logic Framework

Speaker: Lars Birkedal, Professor of Computer Science at Aarhus University

Abstract:
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<http://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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211202/c98ab19d/attachment-0001.html>