Don't Call Us, We'll Call You: Towards Mixed-Initiative Interactive Proof Assistants for Programming Language Theory

Jan Liam Verter, Tomas Petricek

There are two kinds of systems that programming language researchers use for their work. Semantics engineering tools let them interactively explore their definitions, while proof a…