Scrap your boilerplate definitions in 10 lines of Ltac!
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.
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00
|A Visual Ltac Debugger in CoqIDERemote|
S: Jim Fehrle NoneFile Attached
|Scrap your boilerplate definitions in 10 lines of Ltac!InPerson|
|Tealeaves: Categorical structures for syntaxInPerson|
S: Lawrence Dunn University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Val Tannen University of Pennsylvania, USAFile Attached
|Towards a Formalization of Nominal Sets in CoqRemote|
|A Case for Lightweight Interfaces in CoqInPerson|
David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock SystemsFile Attached