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

Mechanized metatheory proofs often feature many similar proof obligations which Coq users can automatically discharge using Ltac. Unfortunately, there is no comparable solution to help users state many similar lemmas or write inductive definitions with many closely related cases. This talk presents IDT, a Coq library for automatically generating these sorts of boilerplate definitions, powered by Template-Coq and using Ltac to do all the heavy lifting. We give several examples of IDT in action, drawn from a formalization of a language for oblivious computation. Using IDT, we can generate dozens of definitions from just a few lines of Ltac.

Abstract (coqpl22-final16.pdf)394KiB

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