ICFP/SPLASH 2025 (series) / HATRA 2025 (series) / Human Aspects of Types and Reasoning Assistants (HATRA 2025) /
Actema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction
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.
Tue 14 OctDisplayed time zone: Perth change
Tue 14 Oct
Displayed time zone: Perth change
13:40 - 15:20 | |||
13:40 25mTalk | Negative Bounds for Avoiding Conflicts in Implementing Traits in Rust HATRA Link to publication | ||
14:05 25mTalk | P4-SpecTec: A Language Mechanization Framework for P4 HATRA | ||
14:30 25mTalk | Types as a Specification Language for Creativity HATRA Youyou Cong Institute of Science Tokyo Link to publication | ||
14:55 25mTalk | Actema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction HATRA |