1. Top
  2. 6.5610-project
  3. Commits
6.5610-project

Cryptography final project

Commits at f1c8b8e7da9d0cde6e7991916c7a087e57e203e0

  1. 56b19849 Implement Fibonacci in μLean Anthony Wang authored at Anthony Wang comitted at
  2. f63c5d98 Fix soundness bug in slop code too Anthony Wang authored at Anthony Wang comitted at
  3. 31ad5e7c Fixed another soundness bug whew Anthony Wang authored at Anthony Wang comitted at
  4. ac2e7867 Delete Lurk files for old type checker I kept the demo directory though Anthony Wang authored at Anthony Wang comitted at
  5. 9fb51f49 Comment about runtime Anthony Wang authored at Anthony Wang comitted at
  6. 2b9156e0 Port the dependent type checker to Lurk and Python Yeah it's AI slop but seems to work 🤷 Anthony Wang authored at Anthony Wang comitted at
  7. 0d7bae04 Bump Lean version, fill in missing gensym proof using mvcgen magic Anthony Wang authored at Anthony Wang comitted at
  8. b1d1c7a3 Add a few more random comments I guess idk Anthony Wang authored at Anthony Wang comitted at
  9. 8fcd0127 Compute dbtypes at compile time Anthony Wang authored at Anthony Wang comitted at
  10. 0a32f314 Implement capture-avoiding substitution, add some more (AI slop) proofs Anthony Wang authored at Anthony Wang comitted at
  11. abce03d8 Add addition proofs, fix some soundness bugs Anthony Wang authored at Anthony Wang comitted at
  12. 1c358f55 Fix typos Anthony Wang authored at Anthony Wang comitted at
  13. b04f04b5 Even more comments yay Anthony Wang authored at Anthony Wang comitted at
  14. 9a5750d2 More comments Anthony Wang authored at Anthony Wang comitted at
  15. a2f5f3cf Prove a few more arithmetic-related things Anthony Wang authored at Anthony Wang comitted at
  16. 540e2cfc Remove ap from eval, add mul and pow, fix dependent products and cum univs Anthony Wang authored at Anthony Wang comitted at
  17. 3b014ccc Type checker is almost done hopefully Anthony Wang authored at Anthony Wang comitted at
  18. a99cea45 Add support for variable names Anthony Wang authored at Anthony Wang comitted at
  19. 5165d725 toString for new type checker Anthony Wang authored at Anthony Wang comitted at
  20. 9e5da10a Better notation Anthony Wang authored at Anthony Wang comitted at
  21. 23dd54fb demo Rey Li authored at Rey Li comitted at
  22. 0cb4fc63 Commit more bad code Anthony Wang authored at Anthony Wang comitted at
  23. 3ff64e64 Cursed dependent type stuff Anthony Wang authored at Anthony Wang comitted at
  24. 631afd86 Fix bug in Lurk port as well Anthony Wang authored at Anthony Wang comitted at
  25. 2150026d Prove that uLean type checker is as consistent as Lean Dan Klishch authored at Dan Klishch comitted at
  26. e7a247de Lean type checker bug fix Dan Klishch authored at Dan Klishch comitted at
  27. b699a330 Move Lurk files to root dir, try with a larger proof, delete old garbage Anthony Wang authored at Anthony Wang comitted at
  28. c5d06832 More slightly nontrivial proofs Anthony Wang authored at Anthony Wang comitted at
  29. e0867123 Small tweaks to Lean impl of μLean Anthony Wang authored at Anthony Wang comitted at
  30. 3bb5cccf successful (inelegant) protocol implementation Rey Li authored at Rey Li comitted at