POPL 2021 (series) / CoqPL 2021 (series) / The Seventh International Workshop on Coq for Programming Languages /
Record Updates in Coq
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
Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30 | |||
16:00 15mTalk | A Limited Case for Reification by Type Inference CoqPL Jason GrossMIT CSAIL Media Attached File Attached | ||
16:15 15mTalk | Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml CoqPL File Attached | ||
16:30 15mTalk | Record Updates in Coq CoqPL Tej ChajedMassachusetts Institute of Technology, USA Media Attached File Attached | ||
16:45 15mBreak | Break CoqPL | ||
17:00 15mTalk | The B+-tree Index as a Verified Software Unit CoqPL Anastasiya Kravchuk-KirilyukHarvard University, Andrew AppelPrinceton, Lennart BeringerPrinceton University File Attached | ||
17:15 15mTalk | 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 |