Principles of Programming Seminar

Thursday, October 13, 2016 -
3:30pm to 4:30pm

Location:

8102 Gates & Hillman Centers

Speaker:

IAN VOYSEY, Institute for Software Research /IAN%20VOYSEY

Event Website:

https://www.cs.cmu.edu/Groups/pop/seminar.html

For More Information, Contact:

angieb@cs.cmu.edu

In this talk I will present Hazelnut, a structure editor based on a small bidirectionally typed lambda calculus extended with holes and an internal notion of a cursor. Existing structure editors only guarantee a weak syntactic well-formedness. Hazelnut goes one step further: the possible edit actions maintain static well-definedness. Naively, this prohibition on ill-typed edit states would force the programmer to construct terms in a rigid outside-in manner. To avoid this problem, the semantics of edit actions automatically places terms assigned a type that is inconsistent with the expected type inside a hole. This safely defers the type consistency check until the programmer finishes constructing the term inside the hole. Hazelnut is a foundational type-theoretic account of typed structure editing, rather than an end-user tool itself. To that end, I will describe how Hazelnut's rich metatheory, which is fully mechanized in Agda, guides the definition of an extension to the calculus. I will also discuss future work considering plausible evaluation strategies for terms with holes, and reveal connections with gradual typing and contextual modal type theory. Finally, I will discuss how Hazelnut's semantics lends itself to implementation as a functional reactive program in js_of_ocaml. Hazelnut is joint work with Cyrus Omar, Michael Hilton, Jonathan Aldrich, and Matthew Hammer. — Ian Voysey received his Bachelor's degree in Computer Science and Discrete Mathematics and Logic from Carnegie Mellon University in 2010. He helped to develop the introductory functional programming courses there, and won the inaugural A. Nico Habermann Educational Service Award for that work. His research interests are in mechanized proof, proof theory, and type theory. He is currently a Research Programmer at Carnegie Mellon University. Faculty Host: Jonathan Aldrich

Keywords:

Seminar Series