POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sat 20 Jan 2024 16:22 - 16:45 at Kelvin Lecture - Session 4

Designing user interfaces for interactive theorem provers is as challenging as it is necessary. While being one of the most widely used proof assistants out there, Coq still suffers from the lack of a solid and unified IDE. This becomes particularly problematic when it comes to onboarding new users. In this work, we present VsCoq 2, a full reimplementation of the classic vscode extension. It benefits from the addition of a standalone language server which heavily relies on the seperation between parsing and execution to allow a smooth experience.