Hazel Grove

We are designing Hazel, a structure editor rooted in the principles of type theory.



Research Vision

Toward Semantic Foundations for Program Editors (draft)


To start, we have developed a core calculus, Hazelnut, that establishes 1) principles for reasoning statically in the presence of holes and type inconsistencies, and 2) a semantics of typed edit actions.

Research Paper (POPL 2017)

Hazelnut is described in a research paper, Hazelnut: A Bidirectionally Typed Structure Editor Calculus, which was published at POPL 2017 [.bib]. The presentation slides are available (and a video should be available soon!)


We have mechanized the metatheory of Hazelnut using the Agda proof assistant.


HZ is a simple reference implementation of Hazelnut, written in OCaml and compiled to JavaScript using js_of_ocaml.

Hazelnut Live

We are currently working to understand how one might run the incomplete programs that Hazelnut produces, and how one might interact with these running programs.

Workshop Presentation

An extended abstract and annotated slides for a talk on this topic given by Ian at the Off the Beaten Track (OBT) workshop at POPL 2017 are available.


If you're interested in working on Hazel, in any capacity, get in touch!


Carnegie Mellon University


Carnegie Mellon University


Oregon State University


Carnegie Mellon University


University of Colorado Boulder


We are grateful for the pro bono artistic services provided by Vincent Zeng.

This webpage built with: Bootstrap, Font Awesome, and JQuery