This program is tentative and subject to change.

Sat 22 Jan 2022 10:20 - 10:40 at Salon I - Contributed Talks (Morning) Chair(s): Benjamin C. Pierce

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

This program is tentative and subject to change.

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 12:00
Contributed Talks (Morning)CoqPL at Salon I
Chair(s): Benjamin C. Pierce University of Pennsylvania
10:20
20m
Talk
A Visual Ltac Debugger in CoqIDERemote
CoqPL
S: Jim Fehrle None
File Attached
10:40
20m
Talk
Scrap your boilerplate definitions in 10 lines of Ltac!InPerson
CoqPL
S: Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
File Attached
11:00
20m
Talk
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
20m
Talk
Towards a Formalization of Nominal Sets in CoqRemote
CoqPL
S: Fabrício S. Paranhos Universidade Federal de Goiás, Daniel Ventura Universidade Federal de Goiás
File Attached
11:40
20m
Talk
A Case for Lightweight Interfaces in CoqInPerson
CoqPL
David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock Systems
File Attached
Hide past events