We are designing Hazel, a structure editor rooted in the principles of type theory.
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, 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 are currently working to understand how one might run the incomplete programs that Hazelnut produces, and how one might interact with these running programs.
If you're interested in working on Hazel, in any capacity, get in touch!