Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 16:30 - 16:45 at CoqPL - Contributed Talks

We describe the implementation of coq-record-update, a library that generates functions to set and update fields of Coq records to complement Coq’s existing support for field projections. The implementation abuses features of Coq typeclasses and is thus fun to describe. The library has industrial and academic users that are not in the authors’ institution, which lends credibility to the assertion that it is useful.

Abstract (coqpl21-final3.pdf)339KiB

Tue 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30
Contributed TalksCoqPL at CoqPL
16:00
15m
Talk
A Limited Case for Reification by Type Inference
CoqPL
Jason Gross MIT CSAIL
Media Attached File Attached
16:15
15m
Talk
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
CoqPL
Xuanrui Qi Nagoya University, Jacques Garrigue Nagoya University
File Attached
16:30
15m
Talk
Record Updates in Coq
CoqPL
Tej Chajed Massachusetts Institute of Technology, USA
Media Attached File Attached
16:45
15m
Break
Break
CoqPL

17:00
15m
Talk
The B+-tree Index as a Verified Software Unit
CoqPL
Anastasiya Kravchuk-Kirilyuk Harvard University, Andrew Appel Princeton, Lennart Beringer Princeton University
File Attached
17:15
15m
Talk
Automated Synthesis of Verified Firewalls
CoqPL
Shardul Chiplunkar Massachusetts Institute of Technology, Clément Pit-Claudel Massachusetts Institute of Technology, USA, Adam Chlipala Massachusetts Institute of Technology
File Attached