Agenda

Cuándo: Jueves 4 de julio, a las 11:00 horas.

Dónde: Sala Ada Lovelace (3er. Piso, Torre Poniente, Beauchef 851, Santiago)

Organiza: Éric Tanter, académico Departamento Ciencias de la Computación Universidad de Chile, investigador asociado IMFD.

Abstract: As a research area, gradual typing has grown considerably over the last decade, with more than 150 papers in the Gradual Typing Bibliography. There are a large number of alternative language designs that have been proposed for gradual typing, and there are many interesting approaches for addressing the efficiency challenges. To better understand and categorize the research on gradual typing, I’ve begun developing an encyclopedia of gradual typing that is mechanized using the Agda proof assistant. In this talk I give an overview the research landscape of gradual typing through the lense of this encyclopedia and report on several abstractions that I have identified that capture similarities and enable the reuse of definitions and theorems across different designs.

Speaker: Jeremy Siek is a Professor at Indiana University. Jeremy’s interests include programming language design, type systems, mechanized theorem proving, and optimizing compilers. Jeremy’s Ph.D. thesis explored foundations for constrained templates, aka the «concepts» proposal for C++. Prior to that, Jeremy developed the Boost Graph Library, a C++ generic library for graph algorithms and data structures. Jeremy post-doc’d at Rice University where he and Walid Taha developed the idea of gradual typing: a type system that integrates both dynamic and static typing in the same programming language. Jeremy taught at the University of Colorado for many years and then moved to Indiana University. Jeremy is currently working on several open questions regarding gradual typing. Is it possible to create a high-performance implementation of a gradually-typed language? Is there an intuitive specification for when a higher-order cast should fail? In 2009 Jeremy received the NSF CAREER award to fund his project: «Bridging the Gap Between Prototyping and Production». In 2010 and again in 2015, Jeremy was awarded a Distinguished Visiting Fellowship from the Scottish Informatics & Computer Science Alliance. From 2015 to the present Jeremy has been working with colleagues at Northeastern, Brown, and Maryland on the NSF-funded projects Gradual Typing Across the Spectrum and Performant Sound Gradual Typing.