Mini-project choice

• See Proof assistants > Mini-project.

A last review of rev_rev proof?

• see new hints for finding the right auxillary lemmas (including graphic idea of the first lemma)
• and/or execute a live proof of another lemma in same theory?
• students asked for a proof of mc_flatten lemma (like last year!)

PVS higher order logic

• Higher order functions and formulas, PVS type hierarchy, predicate subtyping, dependant types, declarations and definitions, constant vs parameter style, theorems, axioms:
• PVS language handout html | pdf (slides 7--23);
• see also PVS language summary;
• axiom danger: ~gloess/pvs/intro/danger.pvs;
• Subtyping and Type Checking Conditions (TCC)s:
• a simple exercise: ~gloess/pvs/intro/simple_exercise.pvs;
• TCCs are not axioms! They are "proof obligations": they require a proof;
• see also PVS language summary.

PVS Recursive functions and well founded induction

• Recursive functions and well founded relations, PVS language handout html | pdf (24--27);
• [additional reading [hard]: PVS formalization of recursive functions (based on fixpoint induction)];
• Well founded induction and generalization, PVS inference handout html | pdf (28--31).

Correctness of a compiler of algebraic expressions into machine code?  not done

• see compiler in Bordeaux PVS applications (LaBRI page: Warning! Some links are no longer operational);
• dump available at ENSEIRB:
• ~gloess/pvs/2.4/compiler/2.4.compiler.24jan2002.dump.dmp