BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Abstracting Gradual Typing
DTSTART:20160628T120000
DTEND:20160628T130000
DTSTAMP:20260407T230504Z
UID:cc8866a780c683864dd67695ee192450dc4b874009ef03b08b04a4e2
CATEGORIES:Conferences - Seminars
DESCRIPTION:Éric Tanter\, University of Chile\n(joint work with Ronald Ga
 rcia and Alison Clark\, presented at POPL’16)Abstract:\nLanguage researc
 hers and designers have extended a wide variety of type systems to support
  gradual typing\, which enables languages to seamlessly combine dynamic an
 d static checking. These efforts consistently demonstrate that designing a
  satisfactory gradual counterpart to a static type system is challenging\,
  and this challenge only increases with the sophistication of the type sys
 tem. Gradual type system designers need more formal tools to help them con
 ceptualize\, structure\, and evaluate their designs.\nWe propose a new for
 mal foundation for gradual typing\, drawing on principles from abstract in
 terpretation to give gradual types a semantics in terms of pre-existing st
 atic types. Abstracting Gradual Typing (AGT for short) yields a formal acc
 ount of consistency---one of the cornerstones of the gradual typing approa
 ch---that subsumes existing notions of consistency\, which were developed 
 through intuition and ad hoc reasoning.\nGiven a syntax-directed static ty
 ping judgment\, the AGT approach induces a corresponding gradual typing ju
 dgment. Then the subject-reduction proof for the underlying static discipl
 ine induces a dynamic semantics for gradual programs defined over source-l
 anguage typing derivations. The AGT approach does not recourse to an exter
 nally justified cast calculus: instead\, run-time checks naturally arise b
 y deducing evidence for consistent judgments during proof-reduction.\nGrad
 ual languages designed with the AGT approach satisfy\, by construction\, t
 he refined criteria for gradual typing set forth by Siek and colleagues.\n
 Time permitting\, we will report on recent developments in applying AGT to
  different typing disciplines\, such as effects and security typing.Bio:\n
 Éric Tanter is a Full Professor in the Computer Science Department of the
  University of Chile\, where he founded the PLEIAD laboratory. He received
  his PhD from both the University of Nantes and the University of Chile in
  2004. His research interests cover programming languages and software eng
 ineering\, ranging from the theoretical underpinnings of programming langu
 ages to the empirical study of the practice of programming.
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR