We are designing Hazel, a structure editor rooted in the principles of type theory.
Our research vision is described in the following paper, which will be presented at SNAPL 2017 in early May.
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.
Hazelnut is described in a research paper published at POPL 2017.
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.
We are grateful for the pro bono artistic services provided by Vincent Zeng.