Skip to content

Files

Latest commit

Jan 2, 2019
08f7e0a · Jan 2, 2019

History

History
This branch is 2 commits ahead of, 67 commits behind opprop/units-inference:master.

coq-proof

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
Apr 7, 2018
Jan 2, 2019
Jan 2, 2019
Apr 9, 2018
Jan 2, 2019
Jan 2, 2019
Apr 7, 2018
Apr 9, 2018
Jan 2, 2019
Jan 2, 2019
Jan 2, 2019
Apr 7, 2018
Apr 7, 2018
Dec 31, 2018
Dec 31, 2018
Apr 7, 2018
May 10, 2018
Jan 2, 2019
Dec 31, 2018

The scripts contained in this folder were tested on ubuntu 18.04 LTS, it is intended to be run on linux.

Setup

run ./setup-coq.sh to download and install Coq v8.8.0 along with its dependencies

Check pUnits proofs

run ./compile.sh

Clean up

run ./cleanup.sh to remove coq output files

Proof file structure

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.