Miller, Dale Mechanized metatheory revisited. (English) Zbl 1468.68303 J. Autom. Reasoning 63, No. 3, 625-665 (2019). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{D. Miller}, J. Autom. Reasoning 63, No. 3, 625--665 (2019; Zbl 1468.68303) Full Text: DOI Link
Farmer, William M. Incorporating quotation and evaluation into Church’s type theory. (English) Zbl 1390.68168 Inf. Comput. 260, 9-50 (2018). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{W. M. Farmer}, Inf. Comput. 260, 9--50 (2018; Zbl 1390.68168) Full Text: DOI arXiv
Rabe, Florian The future of logic: foundation-independence. (English) Zbl 1436.03179 Log. Univers. 10, No. 1, 1-20 (2016). MSC: 03B70 03B22 03B16 PDFBibTeX XMLCite \textit{F. Rabe}, Log. Univers. 10, No. 1, 1--20 (2016; Zbl 1436.03179) Full Text: DOI
Hickey, Jason; Nogin, Aleksey; Yu, Xin; Kopylov, Alexei Practical reflection for sequent logics. (English) Zbl 1278.68263 Momigliano, Alberto (ed.) et al., Proceedings of the first international workshop on logical frameworks and meta-languages: theory and practice (LFMTP 2006), Seattle, WA, USA, August 16, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 5, 79-94 (2007). MSC: 68T15 03B70 PDFBibTeX XMLCite \textit{J. Hickey} et al., Electron. Notes Theor. Comput. Sci. 174, No. 5, 79--94 (2007; Zbl 1278.68263) Full Text: Link
Hickey, Jason; Nogin, Aleksey; Yu, Xin; Kopylov, Alexei Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection. (English) Zbl 1321.68194 Proceedings of the 11th ACM SIGPLAN international conference on functional programming, ICFP ’06, Portland, OR, USA, September 18–20, 2006. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-59593-309-3). ACM SIGPLAN Notices 41, No. 9, 172-183 (2006). MSC: 68N30 68N15 PDFBibTeX XMLCite \textit{J. Hickey} et al., in: Proceedings of the 11th ACM SIGPLAN international conference on functional programming, ICFP '06, Portland, OR, USA, September 18--20, 2006. New York, NY: Association for Computing Machinery (ACM). 172--183 (2006; Zbl 1321.68194) Full Text: DOI
Schürmann, C.; Despeyroux, J.; Pfenning, F. Primitive recursion for higher-order abstract syntax. (English) Zbl 0994.68028 Theor. Comput. Sci. 266, No. 1-2, 1-57 (2001). MSC: 68N18 PDFBibTeX XMLCite \textit{C. Schürmann} et al., Theor. Comput. Sci. 266, No. 1--2, 1--57 (2001; Zbl 0994.68028) Full Text: DOI
Rueß, Harald Reflection of formal tactics in a deductive reflection framework. (English) Zbl 1412.68257 McRobbie, M. A. (ed.) et al., Automated deduction – CADE-13. 13th international conference on automated deduction, New Brunswick, NJ, USA, July/August 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1104, 628-642 (1996). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{H. Rueß}, Lect. Notes Comput. Sci. 1104, 628--642 (1996; Zbl 1412.68257) Full Text: DOI
Paulson, Lawrence C. Set theory for verification. I: From foundations to functions. (English) Zbl 0802.68128 J. Autom. Reasoning 11, No. 3, 353-389 (1993). MSC: 68T15 03E75 03-04 PDFBibTeX XMLCite \textit{L. C. Paulson}, J. Autom. Reasoning 11, No. 3, 353--389 (1993; Zbl 0802.68128) Full Text: DOI