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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30: Contributed TalksCoqPL at CoqPL
16:00 - 16:15
Talk
A Limited Case for Reification by Type Inference
CoqPL
Jason GrossMIT CSAIL
Media Attached File Attached
16:15 - 16:30
Talk
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
CoqPL
Xuanrui QiNagoya University, Jacques GarrigueNagoya University
File Attached
16:30 - 16:45
Talk
Record Updates in Coq
CoqPL
Tej ChajedMassachusetts Institute of Technology, USA
Media Attached File Attached
16:45 - 17:00
Break
Break
CoqPL
17:00 - 17:15
Talk
The B+-tree Index as a Verified Software Unit
CoqPL
Anastasiya Kravchuk-KirilyukHarvard University, Andrew AppelPrinceton, Lennart BeringerPrinceton University
File Attached
17:15 - 17:30
Talk
Automated Synthesis of Verified Firewalls
CoqPL
Shardul ChiplunkarMassachusetts Institute of Technology, Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Adam ChlipalaMassachusetts Institute of Technology
File Attached