A brief overview over our IL/M formalisation:
We used Coq 8.4 for our development. Run "make" in the root folder to compile
all source files. The "configure" script was used to generate the Makefile.
Note that we make heavy use of the Coq 8.4 proof structure features, so the
files are not compatible with previous versions of Coq.

The files in the subfolders (constr/, il/, infra/, isa/) are taken almost
verbatim from the original IL/F formalisation by Schneider [1] which is based
on a compiler verification Research Immersion Lab [2]. Only some minor
modifications were performed.
* infra/ provides some generally useful tools, like tactics to do case
  distinction over decidable equalities.
* constr/ provides axiomatic descriptions of finite sets and maps, plus many
  useful lemmas (especially about sets) derived from the basic axioms.
* il/ defines variables and environments.
* isa/ provides axioms about types, values and expressions.

The files in the root constitute the actual formalisation of IL/M:
* ILM.v contains the syntax as well as the small-step and big-step semantics
  and a proof that semantics are deterministic. This corresponds to
  Section 3.4.
* ILM_Types.v provides the type system and the definition of state consistency.
  This corresponds to Section 4.2 and 5.1, except for the proof of type
  preservation.
* ILM_Preservation.v contains the proof of type preservation
  (Theorem 1 of the thesis).
* ILM_Equivalences.v contains proofs for simple semantic equivalences (like
  swapping independent store operations) as well as the definition of
  normalisation and the proof that well-typed programs are semantically
  equivalent to their normalised form (Theorem 2 in the thesis).
  This corresponds to Section 5.2.
These files also contain comments relating Coq definitions and lemmas to the
thesis.


[1] Sigurd Schneider. 'Semantics of an Intermediate Language for Program
    Transformation'. Master's Thesis. Saarland University, 2013.
[2] https://public.cdl.uni-saarland.de/redmine/projects/ril-cv-12
