This program is tentative and subject to change.

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

Despite nominal techniques have stood the test of time, no nominal framework has been proposed for the Coq proof assistant. A work in progress formalization of nominal sets in Coq is presented, highlighting the main design decisions. Type classes and generalized rewriting mechanisms, also known as setoid rewriting, allows concise definitions and proofs, whilst avoiding the well-known “setoid hell” scenario. The present work is a first step for a nominal package for Coq.

Abstract (coqpl22-final52.pdf)434KiB

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