This program is tentative and subject to change.

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

Large-scale developments rely on separate compilation to enable modular reasoning for both developers and compilers: When working on clients of a compilation unit, both developers and compilers can review its interface rather than its implementation. While Coq offers several modularity mechanisms, including ML-style modules, we have found its lack of lightweight support for separating interfaces from implementations to hinder scaling Coq to industrial developments. While our experience is with C++ program verification, we believe the problem is of general interest.

Abstract (coqpl22-final78.pdf)384KiB

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