Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/Proof_by_Reflection.txt

Created July 31, 2023 16:25
Show Gist options
  • Save mukeshtiwari/769af9477c651f0872164481e1a277e9 to your computer and use it in GitHub Desktop.
Save mukeshtiwari/769af9477c651f0872164481e1a277e9 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Proof_by_Reflection.txt
https://coq.github.io/doc/V8.11.1/refman/addendum/ring.html
http://poleiro.info/posts/2015-04-13-writing-reflective-tactics.html
https://www.cs.ox.ac.uk/ralf.hinze/publications/TFP09.pdf
https://link.springer.com/chapter/10.1007/978-3-540-30142-4_17
https://dspace.mit.edu/bitstream/handle/1721.1/137403/2018-reification-by-parametricity-itp-draft.pdf?sequence=2&isAllowed=y
https://github.com/coq/coq/blob/v8.18/theories/setoid_ring/Ring_polynom.v
Proving Equalities in a Commutative Ring Done Right in Coq
http://adam.chlipala.net/papers/ReificationITP18/ReificationITP18.pdf
https://github.com/mit-plv/reification-by-parametricity
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment