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.
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
10:30 - 12:30
|Deriving Instances with Dependent Types|
Arthur Azevedo de Amorim Carnegie Mellon University, USAFile Attached
|The use of Coq for Common Criteria Evaluations|
Yves Bertot INRIA, Maxime Dénès Inria, Vincent Laporte Inria, Arnaud Fontaine ANSSI, Thomas Letan ANSSIFile Attached
|Verifying concurrent Go code in Coq with Goose|
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, USALink to publication File Attached
|A Tutorial on Equations|
Matthieu Sozeau InriaMedia Attached File Attached