Formalizing Monoidal Categories and Actions for Syntax with Binders (CoqPL 2023 - The Ninth International Workshop on Coq for Programming Languages)

Sun 15 - Sat 21 January 2023 Boston, Massachusetts, United States

Who

Benedikt Ahrens, Ralph Matthes, Kobe Wullaert

Track

CoqPL 2023

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 21 Jan 2023 14:30 - 15:00 at Scollay - Session 3

Abstract

We discuss some aspects of our work on the mechanization of syntax and semantics in the UniMath library, based on the proof assistant Coq. We focus on experiences where Coq (as a type-theoretic proof assistant with decidable type-checking) made us use more theory or helped us to see theory more clearly.

File attachments

Extended abstract (coqpl2023.pdf)	388KiB

Benedikt Ahrens

TU Delft, The Netherlands

Netherlands

Ralph Matthes

IRIT (CNRS and Univ. of Toulouse)

Kobe Wullaert

Technical University Delft