Additional information for interested students:

- Adam Chlipala's book on Certified Programming with Dependent Types: https://adam.chlipala.net/cpdt/html/toc

- Picinae, starting at the strcmp i386 proof: https://github.com/CharlesAverill/Picinae/blob/master/Examples/i386_strcmp_proof.v

- jsCoq: https://coq.vercel.app/scratchpad.html

- My AAL/L* in Rocq repo: https://github.com/charlesaverill/lstar-rocq

- The most pedagogical version of the L* development, linking to the original paper with
  inline references to it (also an example of extracting ocaml code from rocq):
  https://github.com/CharlesAverill/lstar-rocq/blob/dc33043d996382a95de2ea4c5ef198c845fe732e/theories/Lstar.v