PhD Proposal: Towards Structured Proof Editing

Modern programming environments have been developed to include sophisticated interfaces for presenting intermediate information to the user gathered from automated analyses of their program, including linting checks, scoping checks, type checks, and others.One critical aspect of these interfaces is their utility not only for considering completed programs but also for considering incomplete programs.In this way, these interfaces can integrate directly into the editing experience itself, such as presenting the expected type of a function's argument before it is provided, or symbolically executing a program with holes.Additionally, the user can leverage these analyses to help determine which edits to make, or even to perform edits automatically, such as with autocompletion suggestions, symbol renaming and other edit actions in LSPs and IDEs, typed hole refining in Agda, and typed structure editing in Pantograph.The implementation of these types of interfaces for proof assistants is one particularly interesting application.
My goal is to develop a new typed structure editor and proof assistant for interactive proof development.The new system will support a generalized version of structured tree editing, typed edits, and a simple tactic system.To be used as a proof assistant, the system will also support an extensional dependent type theory with typed holes.These novel features bring the structured editing benefits of typed structure editing to interactive proof development in a way confluent with both interactive tactics and hole-driven editing.