POPL 2020 (series) / CoqPL 2020 (series) / The Sixth International Workshop on Coq for Programming Languages /
Deriving Instances with Dependent Types
We present Deriving, a Coq library inspired by the analogous Haskell feature that simplifies the definition of class instances for inductive types. A few declarations suffice to define equality tests for a type or enumerate its elements, and proofs of correctness are provided automatically. The library includes generic implementations of basic classes of the MathComp hierarchy (eqType, choiceType, countType and finType), and can be extended to other classes with user-level code.
| Slides (talk.pdf) | 66KiB |
| (coqpl20-final1.pdf) | 347KiB |
| Coq demo (demo.v) | 8KiB |
I am currently a post-doc researcher at CMU working with Matt Fredrikson and Anupam Datta. I completed my Ph.D. studies at the University of Pennsylvania, under the supervision of Benjamin Pierce.
Sat 25 JanDisplayed time zone: Saskatchewan, Central America change
Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change
10:30 - 12:30 | |||
10:30 30mTalk | Deriving Instances with Dependent Types CoqPL Arthur Azevedo de Amorim Carnegie Mellon University, USA File Attached | ||
11:00 30mTalk | The use of Coq for Common Criteria Evaluations CoqPL Yves Bertot INRIA, Maxime Dénès Inria, Vincent Laporte Inria, Arnaud Fontaine ANSSI, Thomas Letan ANSSI File Attached | ||
11:30 30mTalk | Verifying concurrent Go code in Coq with Goose CoqPL Tej Chajed Massachusetts Institute of Technology, USA, Joseph Tassarotti Boston College, M. Frans Kaashoek Massachusetts Institute of Technology, USA, Nickolai Zeldovich Massachusetts Institute of Technology, USA Link to publication File Attached | ||
12:00 30mTalk | A Tutorial on Equations CoqPL Matthieu Sozeau Inria Media Attached File Attached | ||
