A Case for Lightweight Interfaces in Coq (CoqPL 2022 - The Eighth International Workshop on Coq for Programming Languages)

Sun 16 - Fri 28 January 2022 Philadelphia, Pennsylvania, United States

Who

David Swasey, Paolo G. Giarrusso, Gregory Malecha

Track

CoqPL 2022

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

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

Abstract

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.

File attachments

Abstract (coqpl22-final78.pdf)	384KiB

David Swasey

BedRock Systems

Paolo G. Giarrusso

BedRock Systems

Gregory MalechaSpeaker

BedRock Systems

United States

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

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