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

Coq has been successfully used to support CC formal analysis. The ANSSI and Inria have been collaborating on an authoritative document to introduce guidelines and rules for formal analyses supported by Coq, in order to make these developments easier to read and evaluate. Our main motivation is to clarify our expectations regarding the use of Coq, both for evaluators and developers involved in CC formal analyses. We believe CoqPL is an excellent opportunity to present the result of this work to the Coq community, in the hope to start a discussion and gather feedback.

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