ICFP/SPLASH 2025 (series) / HATRA 2025 (series) / HATRA 2025 /
Actema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction
We present Actema, a graphical user interface for interactive theorem proving that integrates with the Rocq proof assistant through a client-server plugin architecture. Actema enables users to construct formal proofs via direct manipulation actions — such as click and drag-and-drop — upon logical and mathematical expressions in the current proof state, offering an expressive gestural language that extends the Proof-by-Pointing paradigm introduced by Bertot et al. in the 90s.