POPL 2020 (series) / CoqPL 2020 (series) / The Sixth International Workshop on Coq for Programming Languages /
The use of Coq for Common Criteria Evaluations
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.
| (coqpl20-final2.pdf) | 357KiB |
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 | ||