Éric Tanter (University of Chile)
Éric Tanter é Professor Titular e Chefe do Departamento de Ciência da Computação da Universidade do Chile. Ele recebeu seu PhD tanto da Universidade de Nantes e da Universidade do Chile em 2004. Seus interesses acadêmicos estão nas áreas de linguagens de programação e engenharia de software, indo dos fundamentos teóricos de linguagens de programação ao estudo empírico da prática de programação. Ele publicou muitos artigos nas principais conferências e periódicos dessas áreas, e está regularmente envolvido nos comitês de programa e corpos editoriais dos mesmos. Recentemente, ele tem trabalhado principalmente nos fundamentos e prática da tipagem gradual e verificação.
Título do Keynote: The Essence of Gradual Typing
Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and 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 system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs.
We present a formal foundation for gradual typing, drawing on principles from abstract interpretation, to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency—one of the cornerstones of the gradual typing approach—that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning.
Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the subject-reduction proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not recourse to an externally-justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof-reduction.
Gradual languages designed with the AGT approach satisfy, by construction, the established criteria for gradually-typed languages. We report on our experience applying AGT to various typing disciplines, highlighting the challenges of achieving type soundness (and not only type safety) when types are expected to enforce semantic properties like parametricity and noninterference.