Lightning talk: Commanding Emacs from Coq
summary
Defines a monadic eDSL in Coq that models atomic editor actions (get-char, remove-char, insert-char) and builds an Emacs Lisp interpreter that talks to Coq over Proof General, sending vernacular eval requests and interpreting returned strings as editor effects. Uses call-by-need normalization to evaluate embedded expressions, performs reassociation to ensure left-nested binds become atomic, and relies on Coq’s totality/field-based bounds for termination. Targets richer IDE features and is portable to other provers.
AI-written summary · about