Hazel Grove

We are designing Hazel, a programming environment rooted in type theory.

Projects

Try Hazel

Try out our current implementation of Hazel

  • Source code (Reason/Ocaml + Coq, compiled to JavaScript via js_of_ocaml)

Research Vision

Our research vision is described in the following paper, which was presented at SNAPL 2017.

Hazelnut

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 published at POPL 2017.

Mechanization

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

Implementation

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, 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).

LIVE 2017 Paper

A short paper will be presented by Cyrus at the LIVE 2017 workshop at SPLASH on Oct. 24th.

OBT 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.

Team

    

Carnegie Mellon University

    

Carnegie Mellon University

    

Carnegie Mellon University

    

Carnegie Mellon University

    

University of Colorado Boulder


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

Acknowledgements

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