POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 11:20 - 11:45 at Auditorium - Type Systems 1 Chair(s): Avik Chaudhuri

Structure editors allow programmers to edit the tree structure of a program directly. This can have cognitive benefits, particularly for novice and end-user programmers (as evidenced by the popularity of structure editors like Scratch.) It also simplifies matters for tool designers, because they do not need to contend with malformed program text.

This paper defines Hazelnut, a structure editor based on a small bidirectionally typed lambda calculus extended with holes and a cursor (ala Huet’s zipper.) Hazelnut goes one step beyond syntactic well-formedness: it’s edit actions operate over statically meaningful (i.e. well-typed) terms. Naïvely, 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 action semantics 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 term inside the hole is finished.

Hazelnut is a foundational type-theoretic account of typed structure editing, rather than an end-user tool itself. To that end, we describe how Hazelnut’s rich metatheory, which we have mechanized in Agda, guides the definition of an extension to the calculus. We also discuss various plausible evaluation strategies for terms with holes, and in so doing reveal connections with gradual typing and contextual modal type theory (the Curry-Howard interpretation of contextual modal logic.) Finally, we discuss how Hazelnut’s semantics lends itself to implementation as a functional reactive program. Our reference implementation is written using js_of_ocaml .

Wed 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Type Systems 1POPL at Auditorium
Chair(s): Avik Chaudhuri Facebook
10:30
25m
Talk
Polymorphism, subtyping and type inference in MLsub
POPL
Stephen Dolan , Alan Mycroft University of Cambridge
10:55
25m
Talk
Java generics are Turing complete
POPL
Radu Grigore University of Kent
11:20
25m
Talk
Hazelnut: A Bidirectionally Typed Structure Editor Calculus
POPL
Cyrus Omar Carnegie Mellon University, Ian Voysey Carnegie Mellon University, Michael Hilton Oregon State University, USA, Jonathan Aldrich Carnegie Mellon University, Matthew Hammer University of Colorado, Boulder
11:45
25m
Talk
Modules, Abstraction, and Parametric Polymorphism
POPL
Karl Crary Carnegie Mellon University