HenBlocks: Structured Editing for Coq

A block-based structured editor for the Coq Proof Assistant.

Visit HenBlocks
Screenshot of HenBlocks

Introduction

HenBlocks is a web-based fully-fledged structured editor for Coq that I built using the Blockly library and jsCoq. The primary target audience for HenBlocks is undergraduate students who have some experience with functional programming but with little or no experience in proving. The intended use case is for such students to learn, discover, and practise proving with HenBlocks, and eventually transition to writing textual proofs in the Coq Proof Assistant via a text editor such as CoqIDE or Emacs.

HenBlocks was developed as part of my final year undergraduate Capstone project.

Links

Extended Abstract (3 Pages) Full Report Presentation GitHub