Wrapping up

The majority of the work was in reading Logical Foundations and completing the exercises. The most important parts to learn about was proof by induction, tactics, the distinction between Prop and Bool, the Curry-Howard isomorphism, inductive propositions, and more sophisticated tactics. We skimmed Imp.v, it was similar to 15-316’s structural operational semantics and 15-312. We did most of the exercises, including advanced ones.

We define a language for arithmetic and boolean expressions. First, we define the abstract syntax, then the evaluation rules. We also start defining optimizations - like changing every occurence of 0+e to e. These can be defined functionally or as inference rules and inductive propositions, which are equivalent (as proven). There is nuance in choosing the styles - for inductive propositions, inversion and induction works better. Functional definitions are total, deterministic and computable. They can also be extracted from Gallina into OCaml.

We represent a machine state orstate using a total map, mapping variables to their values in a point of execution of a program. We assume the state is defined for all variables - using 0 as the default value in the total map. We then add the syntax for variables.

We then define the commands for Imp. They include skip, assign (x : = a ), sequential composition c;c, conditionals if b then c else c end, and while loops while b do c end.

We have been using a lot of notations for Imp, so the Locate tactic will be helpful in figuring out which is which. Evaluation is better as a relation than a function (result is a Prop instead of a state). This allows for nondeterministic features to the language. We then define the operational semantics of Imp.

Tacticals were introduced as well as strong tactics like lia. The following link is a concise summary of Coq tactics.

https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html

Back to Top