Write a Blog >>
Sat 25 Jan 2020 10:30 - 11:00 at Maurepas - Contributed Talks Chair(s): Amin Timany

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 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 12:30
Contributed TalksCoqPL at Maurepas
Chair(s): Amin Timany imec-Distrinet KU-Leuven
10:30
30m
Talk
Deriving Instances with Dependent Types
CoqPL
Arthur Azevedo de Amorim Carnegie Mellon University, USA
File Attached
11:00
30m
Talk
The use of Coq for Common Criteria Evaluations
CoqPL
File Attached
11:30
30m
Talk
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
30m
Talk
A Tutorial on Equations
CoqPL
Media Attached File Attached