BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verified Software Toolchains: Towards algebraic foundations for al
 ignment - David Naumann (Stevens Institute of Technology)
DTSTART:20220713T140000Z
DTEND:20220713T144500Z
UID:TALK176648@talks.cam.ac.uk
DESCRIPTION:Compositional reasoning about relational properties of program
 s is achieved by aligning intermediate points in pairs of program executio
 ns\, in order to establish relations at those points. Notions of alignment
  have appeared in many guises\, often tied to syntactic alignment of progr
 am points. A precise account of alignment is needed to define alignment co
 mpleteness\, which in turn is needed because the standard logical notion o
 f completeness sheds little light on relational program logics. In this ta
 lk I will review recent work using Kleene algebra with tests (KAT) to expl
 icate and generalize reasoning about alignment.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR