Certified Abstract Interpretation with Pretty-Big-Step Semantics

This page lists the Coq material of this¹ paper.

To illustrate the expandability of the approach, we give two versions: a simple While language—described in the paper—and an extension of it where we added procedures.

This version is closer to the paper description and contains analyzers for a simple While language.

• Link to the Coq code (HTML).
• List of all Coq definitions (HTML).
• Raw results of the analysers (HTML).
• Raw results of the analysers (Org-mode).
• Link to the Coq code (Coq files).

This is a more recent version of the sources, in which procedures have been added. The new concrete semantic rules and domains can be found here. The changes are indicated with a red triangle “△”.

• Link to the Coq code (HTML).
• List of all Coq definitions (HTML).
• Raw results of the analysers (HTML).
• Raw results of the analysers (Org-mode).
• Link to the Coq code (Coq files).