Reflection and its application to mechanized metareasoning about programming languages
It is well known that adding reflective reasoning can tremendously increase the power of a proof assistant. In order for this theoretical increase of power to become accessible to users in practice, the proof assistant needs to provide a great deal of infrastructure to support reflective reasoning....
Internet
https://thesis.library.caltech.edu/1960/1/thesis_xin.pdfYu, Xin (2007) Reflection and its application to mechanized metareasoning about programming languages. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/S0HG-RT72. https://resolver.caltech.edu/CaltechETD:etd-05222007-211909 <https://resolver.caltech.edu/CaltechETD:etd-05222007-211909>