Gunther, Emmanuel; Pagano, Miguel; Sánchez Terraf, Pedro; Steinberg, Matías The formal verification of the ctm approach to forcing. (English) Zbl 07815139 Ann. Pure Appl. Logic 175, No. 5, Article ID 103413, 28 p. (2024). MSC: 68V20 03E35 03E30 03E04 PDFBibTeX XMLCite \textit{E. Gunther} et al., Ann. Pure Appl. Logic 175, No. 5, Article ID 103413, 28 p. (2024; Zbl 07815139) Full Text: DOI arXiv
Gunther, Emmanuel; Pagano, Miguel; Sánchez Terraf, Pedro First steps towards a formalization of forcing. (English) Zbl 1434.03029 Accattoli, Beniamino (ed.) et al., Proceedings of the 13th workshop on logical and semantic frameworks with applications, LSFA 18, Fortaleza, Brazil, September 26–28, 2018. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 344, 119-136 (2019). MSC: 03B35 03E35 68V20 PDFBibTeX XMLCite \textit{E. Gunther} et al., Electron. Notes Theor. Comput. Sci. 344, 119--136 (2019; Zbl 1434.03029) Full Text: DOI arXiv
Arthan, Rob On definitions of constants and types in HOL. (English) Zbl 1356.68173 J. Autom. Reasoning 56, No. 3, 205-219 (2016). MSC: 68T15 PDFBibTeX XMLCite \textit{R. Arthan}, J. Autom. Reasoning 56, No. 3, 205--219 (2016; Zbl 1356.68173) Full Text: DOI