•   When: Wednesday, March 06, 2019 from 10:00 AM to 11:00 AM
•   Speakers: Cyrus Omar
•   Location: Research Hall 163
•   Export to iCal

Abstract:

When programming, it is common to spend minutes, hours, or even days at a time working with program text where there are missing pieces, type errors, or merge conflicts. Programming environments have trouble generating meaningful feedback in these situations because programming languages typically assign formal meaning only to fully-formed, well-typed programs. Lacking timely and meaningful feedback, programmers--particularly novice programmers--struggle to maintain an accurate mental model of the behavior of the code that they are reading and writing, resulting in confusion and costly mistakes.

In this talk, I will introduce Hazel, a live functional programming environment that addresses the problem of working with incomplete programs from type-theoretic first principles. Hazel can synthesize incomplete types for incomplete programs, run incomplete programs to produce incomplete results, and perform various semantic transformations on incomplete programs. These transformations are exposed to the programmer as keyboard-driven semantic edit actions. We have formally specified each of these mechanisms using the Agda proof assistant, resulting in the first end-to-end specification for a live programming environment.

This rich semantic framework lays the foundation for a new generation of intelligent programming environments that automate away boilerplate software development tasks, leaving users to focus only on those tasks that truly require human creativity.

Speaker Bio:

Cyrus Omar leads the Hazel project as a postdoc at The University of Chicago. He received his PhD in Computer Science from Carnegie Mellon University in May 2017, and he started his research career as a neurobiologist before deciding that we need tools that augment human cognition if we are to truly understand human cognition.