ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore

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.