BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Compositional Compiler Verification for a Multi-Language World - A
 mal Ahmed\, Northeastern University
DTSTART:20180615T130000Z
DTEND:20180615T140000Z
UID:TALK105535@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:Verified compilers are typically proved correct under severe r
 estrictions on what the compiled code may be linked with\, from no linking
  at all to linking with only the output of the same compiler.  Unfortunate
 ly\, such assumptions don't match the reality of how we use these compiler
 s as most software today is comprised of components written in different l
 anguages compiled by different compilers to a common target.  A key challe
 nge when verifying correct compilation of components -- or "compositional"
  compiler correctness -- is how to formally state the compiler correctness
  theorem so it supports linking with target code of arbitrary provenance\,
  as well as verification of multi-pass compilers. Recent results state the
 ir correct-component-compilation theorems in remarkably different ways.  W
 orse\, to check if these theorems are sensible\, reviewers must understand
  a massive amount of formalism.\n\nIn this talk\, I will survey recent res
 ults\, discussing pros and cons of their compiler-correctness statements\,
  and then present a generic compositional compiler correctness (CCC) theor
 em that we argue is the desired theorem for any compositionally correct co
 mpiler. Specific compiler-verification efforts can use their choice of for
 malism ``under the hood'' and then show that their theorems imply CCC.  I
 ’ll discuss what CCC reveals about desired properties of proof architect
 ures going forward.  I'll argue that compositional compiler correctness is
 \, in essence\, a language interoperability problem:\nembedding a single-l
 anguage fragment in a multi-language system affects the notion of program 
 equivalence that programmers use when reasoning about their code and that 
 compiler writers use when reasoning about the correctness of compiler opti
 mizations.  For viable\nsolutions in the long term\, we must design langua
 ges that give programmers control over a range of interoperability (linkin
 g) options.\n\nBio: \n\nAmal Ahmed is an Associate Professor of Computer S
 cience at Northeastern University.  Her research interests include type sy
 stems and semantics\, compiler verification\, language interoperability\, 
 dependent types\, and gradual typing.  She is known for her work on scalin
 g the logical relations proof method to realistic languages -- with featur
 es like memory allocation and mutation\, objects\, and concurrency -- lead
 ing to wide use of the technique\, e.g.\, for correctness of compiler tran
 sformations\, soundness of advanced type systems\, and verification of fin
 e-grained concurrent data structures.  Her primary focus of late has been 
 on developing an architecture for building correct and secure compilers th
 at support safe inter-language linking of compiled code. Her awards includ
 e an NSF Career Award and a Google Faculty Research Award.  She has served
  as program chair for ESOP and on the steering committees of ETAPS\, ESOP\
 , PLMW\, and ICFP.  She is also a frequent lecturer at the annual Oregon P
 rogramming Languages Summer School (OPLSS).
LOCATION:FW26
END:VEVENT
END:VCALENDAR