A drag-and-drop proof tactic

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

We explore the features of a user interface where formal proofs can be built through gestural actions. In particular, we show how proof construction steps can be associated to drag-and-drop actions. We argue that this can provide quick and intuitive proof construction steps. This work builds on theoretical tools coming from deep inference. It also resumes and integrates some ideas of the former proof-by-pointing project.

Original languageEnglish
Title of host publicationCPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022
EditorsAndrei Popescu, Steve Zdancewic
PublisherAssociation for Computing Machinery, Inc
Pages197-209
Number of pages13
ISBN (Electronic)9781450391825
DOIs
Publication statusPublished - 11 Jan 2022
Externally publishedYes
Event11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022 - co-located with POPL 2022 - Philadelphia, United States
Duration: 17 Jan 202218 Jan 2022

Publication series

NameCPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022

Conference

Conference11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022 - co-located with POPL 2022
Country/TerritoryUnited States
CityPhiladelphia
Period17/01/2218/01/22

Keywords

  • deep inference
  • formal proofs
  • logic
  • user interfaces

Fingerprint

Dive into the research topics of 'A drag-and-drop proof tactic'. Together they form a unique fingerprint.

Cite this