GitLab

Using this new typing, prove the stronger soundness statement, moving the evaluation to the conclusion of the theorems.

New typing, proved sound. Also, expressions do not contain machine precision anymore in the case of variables

I also simplified the double pattern matchings used in Expressions.v

Port of Interval Validation to mixed precision. Needed some auxiliary lemmas related to the typing of expressions.

Rework evaluation semantics to not be arguing about precondition, make this explicit in the theorem, that we assume it. Admitted proofs that are obvious

Remove some unused lines from Coq development and rework definitions in HOL4 to contain current state of Coq development

Rework Coq proofs, to get rid of specifying precondition validity for execution by adding this as a property of the semantics

Start working on supporting let statements. Therefore add environment simulation relation and prove preservation by small step semantics for it

Add 2 to 3 line comment to every file to explain where it is used and what it contains. Add references to paper where possible