seplogC

The purpose of this webpage is to provide the Coq formalization discussed in:

• JFR 2014 article
• PLPV 2013 paper

Documentation:

• coqdoc-generated documentation (look at "seplogC").
• A more succint documentation focusing on lemmas and tactics used in our case-study:
  • TPP 2013 talk

Formalization:

• Last version [2018-09-07 Fri]: on github
• Older version [2017-10-24 Tue]: seplogC_PolarSSL.tar.gz
  • Requirements: Coq-8.7.0 and MathComp-1.6.2.
  • Installation: see the file SEPLOGCINSTALL in the root directory.