Don't Call Us, We'll Call You: Towards Mixed-Initiative Interactive Proof Assistants for Programming Language Theory. - Jan Liam Verter; Tomas Petricek 001 (CoRR, 2024)