1. 6
  1.  

  2. 4

    Obligatory guide from a top performer in the field:

    http://adam.chlipala.net/cpdt/

    He also has papers on it using phrase “Programs as Proofs.”

    1. 1

      If anyone’s looking for a job in this area, Cambridge University is hiring 3 people to work on mechanizing mathematics with Isabelle (2 mathematicians & 1 computer scientist). Requires a PhD tho.