BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: An Introduction to Iris: Higher-Order Concurrent Se
 paration Logic
DTSTART:20211129T161500
DTEND:20211129T171500
DTSTAMP:20260408T005509Z
UID:c4d34aa8dcb339fa181c276f02cd921eb19d1b3140b5faccbe2dfcc8
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Lars Birkedal - Aarhus University\nVideo of his talk\n\nAb
 stract\nModern programming languages such as Scala\, Java\, and Rust are e
 xamples of concurrent higher-order imperative programming languages.\nIn t
 his talk I will introduce our research on Iris\, a logical framework\, imp
 lemented and verified in the Coq proof assistant\, which can be used for m
 athematical reasoning about safety and correctness of concurrent higher-or
 der imperative programs.\n(See iris-project.org for more about Iris.)\n\nB
 io\nLars Birkedal is Professor of Computer Science at Aarhus University. H
 e received his Ph.D. in Computer Science from Carnegie Mellon University\,
  USA\, in Dec. 1999 and until Dec. 2012 he was at the IT University of Cop
 enhagen\, Denmark. He served as Head of Department of Computer Science in 
 Aarhus from 2014 to 2017.\n\nLars Birkedal is a Fellow of the ACM\, an ele
 cted member of the Royal Danish Academy of Sciences and Letters\, the reci
 pient of a Villum Investigator grant from the Villum Foundation 2019\, the
  Danish Minister of Research Elite Research Award 2015\, and the ACM SIGPL
 AN Milner Award 2013.\nLars Birkedal’s main research interests lie in th
 e area of logic and semantics of programming languages and type theories. 
 Current work focuses on program logics for reasoning about concurrent\, hi
 gher-order\, and imperative programs\; cyber-security\; and type theories 
 with guarded recursion.\n\nMore information
LOCATION:https://epfl.zoom.us/j/67480331564?pwd=djBhZGN2dGtuR09Lb01DK3dwSn
 JLQT099
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR