BEGIN:VCALENDAR
PRODID:-//Grails iCalendar plugin//NONSGML Grails iCalendar plugin//EN
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VEVENT
DTSTAMP:20260528T023719Z
DTSTART;TZID=Australia/Melbourne:20160527T070000
DTEND;TZID=Australia/Melbourne:20160527T090000
SUMMARY:COGENT: A linearly typed programming language for verified systems code
UID:20260607T102640Z-iCalPlugin-Grails@philevents-web-6b96c54f56-bljdq
TZID:Australia/Melbourne
LOCATION:Old Quad\, Parkville\, Australia\, 3010
DESCRIPTION:<p>Toby Murray (Melbourne) will give a talk titled "COGENT: A linearly typed programming language for verified systems code".&nbsp\;</p>\n<p>Abstract:&nbsp\;Systems code underpins the safety and security of many critical systems\,&nbsp\;yet is predominantly written in unsafe languages like C and C++\, whose&nbsp\;unwieldy semantics make verifying code correctness incredibly&nbsp\;effort-intensive.</p>\n<p>In this talk we present the COGENT programming language\, a restricted\,<br>polymorphic\, higher-order\, and purely functional language with linear<br>types and without the need for a trusted runtime or garbage collector.<br>Linear types allow us to assign two equivalent semantics to the<br>language: one imperative\, suitable for efficient C code generation\; and<br>one functional\, suitable for equational reasoning and verification.<br>We discuss our experience using COGENT to build two Linux file systems<br>and to verify functional correctness properties of one of them.<br>Experience to date suggests that verifying COGENT code is significantly<br>easier than for traditional systems code verification\, like the seL4<br>project to which we compare.</p>
ORGANIZER;CN=Shawn Standefer:
METHOD:PUBLISH
END:VEVENT
END:VCALENDAR