BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Compositional Compiler Verification for a Multi-La
 nguage World - Amal Ahmed\, Northeastern Universit
 y
DTSTART;TZID=Europe/London:20180615T140000
DTEND;TZID=Europe/London:20180615T150000
UID:TALK105535AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/105535
DESCRIPTION:Verified compilers are typically proved correct un
 der severe restrictions on what the compiled code 
 may be linked with\, from no linking at all to lin
 king with only the output of the same compiler.  U
 nfortunately\, such assumptions don't match the re
 ality of how we use these compilers as most softwa
 re today is comprised of components written in dif
 ferent languages compiled by different compilers t
 o a common target.  A key challenge when verifying
  correct compilation of components -- or "composit
 ional" compiler correctness -- is how to formally 
 state the compiler correctness theorem so it suppo
 rts linking with target code of arbitrary provenan
 ce\, as well as verification of multi-pass compile
 rs. Recent results state their correct-component-c
 ompilation theorems in remarkably different ways. 
  Worse\, to check if these theorems are sensible\,
  reviewers must understand a massive amount of for
 malism.\n\nIn this talk\, I will survey recent res
 ults\, discussing pros and cons of their compiler-
 correctness statements\, and then present a generi
 c compositional compiler correctness (CCC) theorem
  that we argue is the desired theorem for any comp
 ositionally correct compiler. Specific compiler-ve
 rification efforts can use their choice of formali
 sm ``under the hood'' and then show that their the
 orems imply CCC.  I’ll discuss what CCC reveals ab
 out desired properties of proof architectures goin
 g forward.  I'll argue that compositional compiler
  correctness is\, in essence\, a language interope
 rability problem:\nembedding a single-language fra
 gment in a multi-language system affects the notio
 n of program equivalence that programmers use when
  reasoning about their code and that compiler writ
 ers use when reasoning about the correctness of co
 mpiler optimizations.  For viable\nsolutions in th
 e long term\, we must design languages that give p
 rogrammers control over a range of interoperabilit
 y (linking) options.\n\nBio: \n\nAmal Ahmed is an 
 Associate Professor of Computer Science at Northea
 stern University.  Her research interests include 
 type systems and semantics\, compiler verification
 \, language interoperability\, dependent types\, a
 nd gradual typing.  She is known for her work on s
 caling the logical relations proof method to reali
 stic languages -- with features like memory alloca
 tion and mutation\, objects\, and concurrency -- l
 eading to wide use of the technique\, e.g.\, for c
 orrectness of compiler transformations\, soundness
  of advanced type systems\, and verification of fi
 ne-grained concurrent data structures.  Her primar
 y focus of late has been on developing an architec
 ture for building correct and secure compilers tha
 t support safe inter-language linking of compiled 
 code. Her awards include an NSF Career Award and a
  Google Faculty Research Award.  She has served as
  program chair for ESOP and on the steering commit
 tees of ETAPS\, ESOP\, PLMW\, and ICFP.  She is al
 so a frequent lecturer at the annual Oregon Progra
 mming Languages Summer School (OPLSS).
LOCATION:FW26
CONTACT:Victor Gomes
END:VEVENT
END:VCALENDAR