The scripts contained in this folder were tested on ubuntu 18.04 LTS, it is intended to be run on linux.
run ./setup-coq.sh to download and install Coq v8.8.0 along with its dependencies
run ./compile.sh
run ./cleanup.sh to remove coq output files
TacticalLemmas.v contains tactic notations from the Software Foundations Coq Library, which helps break down proof cases.
Maps.v contains the definitions and lemmas for maps from any key type K to value type V, augmented by a key equality function key_eq.
UnitsDefs.v contains the definitions and lemmas for the unit types T.
ValueDefs.v contains the definitions and lemmas for labeled values v, which are modeled as nats labeled with a unit in Coq.
IDDefs.v contains the definitions and lemmas for field identifiers f.
GammaDefs.v defines gamma as a map from f to T, using the map definitions from Maps.v.
HeapDefs.v defines heap as a map from f to its static field type Tf and runtime value v, using the map definitions from Maps.v.
SubtypingDefs.v contains the definitions and lemmas for the subtype relationship between units qualifiers, and functions such as the least upper bound of units.
GammaHeapCorrespondence.v defines the correspondince between a wellformed gamma and a wellformed heap.
UnitsArithmetics.v defines and proves properties for the arithmetic functions add, multiply, and modulo between units; including the subtype consistent lemmas discussed in the paper.
FieldDefs.v contains the definitions and the proof of progress and preservation helper lemmas for field declarations fd in our language.
ExpressionDefs.v contains the definitions and the proof of progress and preservation helper lemmas for expressions e in our language.
StatementDefs.v contains the definitions and the proof of progress and preservation helper lemmas for assignment statements s in our language.
ProgramDefs.v contains the definitions for programs P in our language, and the overall proof of progress and preservation lemmas.