Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Sun 18 Aug 2019 14:00 - 14:20 at Birch - Research Session 2

Interactive theorem provers like Coq, Agda and Idris allow programmers to ask questions about incomplete programs (or proofs) to Emacs, and get meaningful answers based on types of the missing parts. This turns programming into a conversation between programmers and their compilers, where Emacs acts as an intermediary. However, programmers are limited in the kinds of questions they can ask. Recent work on extensible editor actions leverages metaprogramming techniques to specify how the compiler should answer custom questions, but that requires writing code in Emacs Lisp to glue the compiler and the editor interface because metaprograms can only command the compiler and not the editor itself.

In this talk, I will describe editor metaprogramming, a novel idea of writing metaprograms that command the editor. I define a monadic embedded domain-specific language (eDSL) for editor commands in Coq, which enables composing these commands in meaningful ways, with the full power of Coq! I will write an interpreter for this eDSL in Emacs Lisp, and make Emacs and Coq processes communicate back and forth. Coq computations will be sent back to Coq, and effectful editor actions such as deleting a character and moving the cursor will be executed in Emacs Lisp.

Sun 18 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:40 - 14:50: Research Session 2Scheme at Birch
14:00 - 14:20
Lightning talk: Commanding Emacs from Coq
Joomy KorkutPrinceton University, USA
14:20 - 14:40
Reigniting Fuse, an Online Partial Evaluator for Scheme
Paulette KoronkevichUniversity of British Columbia
14:40 - 15:00
SRFI-167, SRFI-168 and the functional store