BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260917T131502Z
UID:Seminar-pizza-1090@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Qiyi Tang:MAILTO:Qiyi.Tang@liverpool.ac.uk
DTSTART:20231208T140000
DTEND:20231208T150000
SUMMARY:Friday Lunch and Talk Series
DESCRIPTION:Lorenzo Gheri: Concurrent programming, session types, and proof assistants\n\nFormally and correctly reasoning about programs and their behaviour is a challenging and error-prone task. In the case of concurrency, (multiparty) session types have stood the test of time as a specification and verification framework for distributed message-passing systems. However, on the one hand, pen-on-paper proofs have carried limitations and mistakes, thus calling for the mechanised help of proof assistants. On the other hand, the growing scale and the constant evolution of real-world distributed systems call for added flexibility and modularity in session-type specification and verification.\n\n\n\nIn this talk, I will introduce my research on the two non-disjoint topics of proof assistants and session types, for the specification and verification of concurrent programming. I will present some results and discuss future directions.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1090
LOCATION:
END:VEVENT
END:VCALENDAR