Mentions légales du service

Skip to content

Rewrite case study on automatic differentiation

DE VILHENA Paulo Emílio requested to merge auto_diff_paper into master

This branch completely rewrites the case study on reverse mode automatic differentiation. In particular, it makes the following changes:

  1. Code. We make some changes in the style of the [HH] code to allow readability. We also change the representation of constants and variables.
  2. Mathematical definitions. We simplify some mathematical definitions, introduce notation and improve organization.
  3. Specification. We make the specification much more abstract by introducing the predicate [computes]. Other than being easier to read, this version of the specification allows the verification of programs where [diff] is applied to itself.
  4. Verification. We also improve organization of the verification effort and add tactics. (Some proofs still need tidying though.)

Merge request reports