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

This program is tentative and subject to change.

Tue 14 Oct 2025 14:55 - 15:20 at Orchid Small - Session 2

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.

This program is tentative and subject to change.