Tue 18 Jan 2022 11:35 - 12:00 at Salon III - Proof Infrastructure, Rewriting and Automated Reasoning Chair(s): Steve Zdancewic
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 takes over some ideas of the former proof-by-pointing project.
Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change
Tue 18 Jan
Displayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | Proof Infrastructure, Rewriting and Automated ReasoningCPP at Salon III Chair(s): Steve Zdancewic University of Pennsylvania | ||
10:20 25mTalk | CertiStr: A Certified String SolverDistinguished Paper AwardRemote CPP Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Micha Schrader Technische Universität Kaiserslautern DOI Pre-print Media Attached | ||
10:45 25mTalk | Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo RewritingRemote CPP Michael Färber Universität Innsbruck, Austria DOI Pre-print Media Attached File Attached | ||
11:10 25mTalk | An Extension of the Framework Types-To-Sets for Isabelle/HOLRemote CPP Pre-print Media Attached | ||
11:35 25mTalk | A Drag-and-Drop Proof TacticRemote CPP Benjamin Werner Ecole polytechnique, Pablo Donato Ecole polytechnique, Pierre-Yves Strub Ecole Polytechnique DOI Pre-print Media Attached | ||