POPL 2022 (series) / CoqPL 2022 (series) / The Eighth International Workshop on Coq for Programming Languages / A Visual Ltac Debugger in CoqIDE
A Visual Ltac Debugger in CoqIDERemote
The existing command-line Ltac debugger in coqtop provides very limited functionality. A visual debugger is much easier to use and more appropriate for the larger projects undertaken today. This paper describes a visual Ltac debugger added to CoqIDE in Coq 8.15. Most of the Coq changes made to implement the debugger should be readily reusable by other IDEs.
| Abstract (coqpl22-final5.pdf) | 380KiB |
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
Sat 22 Jan
Displayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | |||
10:20 20mTalk | A Visual Ltac Debugger in CoqIDERemote CoqPL File Attached | ||
10:40 20mTalk | Scrap your boilerplate definitions in 10 lines of Ltac!InPerson CoqPL File Attached | ||
11:00 20mTalk | Tealeaves: Categorical structures for syntaxInPerson CoqPL S: Lawrence Dunn University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Val Tannen University of Pennsylvania, USA File Attached | ||
11:20 20mTalk | Towards a Formalization of Nominal Sets in CoqRemote CoqPL File Attached | ||
11:40 20mTalk | A Case for Lightweight Interfaces in CoqInPerson CoqPL David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock Systems File Attached | ||