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, from type-theoretic first principles, how one might run the incomplete programs that Hazelnut produces, and how one might interleave editing with evaluation (i.e. live programming).
A short paper was presented by Cyrus at the LIVE 2017 workshop at SPLASH on Oct. 24th.
We are grateful for the pro bono artistic services provided by Vincent Zeng.