Ketland, Jeffrey Foundations of applied mathematics. I. (English) Zbl 07795320 Synthese 199, No. 1-2, 4151-4193 (2021). MSC: 03E75 03B30 PDFBibTeX XMLCite \textit{J. Ketland}, Synthese 199, No. 1--2, 4151--4193 (2021; Zbl 07795320) Full Text: DOI
Hou, Zhe Fundamentals of logic and computation. With practical automated reasoning and verification. (English) Zbl 1489.68002 Texts in Computer Science. Cham: Springer (ISBN 978-3-030-87881-8/hbk; 978-3-030-87882-5/ebook). x, 221 p. (2021). Reviewer: Marco Benini (Como) MSC: 68-01 03-01 68Q60 68V20 PDFBibTeX XMLCite \textit{Z. Hou}, Fundamentals of logic and computation. With practical automated reasoning and verification. Cham: Springer (2021; Zbl 1489.68002) Full Text: DOI
Unruh, Dominique Post-quantum verification of Fujisaki-Okamoto. (English) Zbl 07666638 Moriai, Shiho (ed.) et al., Advances in cryptology – ASIACRYPT 2020. 26th international conference on the theory and application of cryptology and information security, Daejeon, South Korea, December 7–11, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12491, 321-352 (2020). MSC: 81P94 94A60 68M25 81P10 PDFBibTeX XMLCite \textit{D. Unruh}, Lect. Notes Comput. Sci. 12491, 321--352 (2020; Zbl 07666638) Full Text: DOI
Benzmüller, Christoph; Scott, Dana S. Automating free logic in HOL, with an experimental application in category theory. (English) Zbl 1434.68639 J. Autom. Reasoning 64, No. 1, 53-72 (2020). MSC: 68V15 03B16 03B35 03B60 18A15 PDFBibTeX XMLCite \textit{C. Benzmüller} and \textit{D. S. Scott}, J. Autom. Reasoning 64, No. 1, 53--72 (2020; Zbl 1434.68639) Full Text: DOI Link
Paulson, Lawrence C. Formalising mathematics in simple type theory. (English) Zbl 1528.03098 Centrone, Stefania (ed.) et al., Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18–23, 2016. Cham: Springer. Synth. Libr. 407, 437-453 (2019). MSC: 03B35 03A05 03B38 68V20 PDFBibTeX XMLCite \textit{L. C. Paulson}, Synth. Libr. 407, 437--453 (2019; Zbl 1528.03098) Full Text: DOI arXiv
Buss, Samuel R. (ed.); Iemhoff, Rosalie (ed.); Kohlenbach, Ulrich (ed.); Rathjen, Michael (ed.) Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5–11, 2017. (English) Zbl 1409.00077 Oberwolfach Rep. 14, No. 4, 3121-3183 (2017). MSC: 00B05 00B25 03Fxx 03-06 PDFBibTeX XMLCite \textit{S. R. Buss} (ed.) et al., Oberwolfach Rep. 14, No. 4, 3121--3183 (2017; Zbl 1409.00077) Full Text: DOI
Benzmüller, Christoph; Scott, Dana Automating free logic in Isabelle/HOL. (English) Zbl 1434.68638 Greuel, Gert-Martin (ed.) et al., Mathematical software – ICMS 2016. 5th international conference, Berlin, Germany, July 11–14, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9725, 43-50 (2016). MSC: 68V15 03B16 03B35 03B60 18A15 PDFBibTeX XMLCite \textit{C. Benzmüller} and \textit{D. Scott}, Lect. Notes Comput. Sci. 9725, 43--50 (2016; Zbl 1434.68638) Full Text: DOI
Hales, Thomas C. Developments in formal proofs. (English) Zbl 1356.03003 Séminaire Bourbaki. Volume 2013/2014. Exposés 1074–1088. Paris: Société Mathématique de France (SMF) (ISBN 978-2-85629-804-6/hbk). Astérisque 367-368, 387-410, Exp. No. 1086 (2015). MSC: 03-02 03B35 03B15 68T15 PDFBibTeX XMLCite \textit{T. C. Hales}, Astérisque 367--368, 387--410, Exp. No. 1086 (2015; Zbl 1356.03003) Full Text: arXiv
Sternagel, Christian Certified Kruskal’s tree theorem. (English) Zbl 1426.68289 J. Formaliz. Reason. 7, No. 1, 45-62 (2014). MSC: 68V20 03B30 03F35 PDFBibTeX XMLCite \textit{C. Sternagel}, J. Formaliz. Reason. 7, No. 1, 45--62 (2014; Zbl 1426.68289) Full Text: DOI
Sternagel, Christian Certified Kruskal’s tree theorem. (English) Zbl 1426.68288 Gonthier, Georges (ed.) et al., Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8307, 178-193 (2013). MSC: 68V20 03B30 03F35 PDFBibTeX XMLCite \textit{C. Sternagel}, Lect. Notes Comput. Sci. 8307, 178--193 (2013; Zbl 1426.68288) Full Text: DOI
Geuvers, Herman; Nederpelt, Rob N. G. de Bruijn’s contribution to the formalization of mathematics. (English) Zbl 1359.03003 Indag. Math., New Ser. 24, No. 4, 1034-1049 (2013). MSC: 03-03 03B35 03B40 01A70 68T15 PDFBibTeX XMLCite \textit{H. Geuvers} and \textit{R. Nederpelt}, Indag. Math., New Ser. 24, No. 4, 1034--1049 (2013; Zbl 1359.03003) Full Text: DOI
Braun, Gabriel; Narboux, Julien From Tarski to Hilbert. (English) Zbl 1397.03019 Ida, Tetsuo (ed.) et al., Automated deduction in geometry. 9th international workshop, ADG 2012, Edinburgh, UK, September 17–19, 2012. Revised selected papers. Berlin: Springer (ISBN 978-3-642-40671-3/pbk). Lecture Notes in Computer Science 7993. Lecture Notes in Artificial Intelligence, 89-109 (2013). MSC: 03B35 03B30 68T15 PDFBibTeX XMLCite \textit{G. Braun} and \textit{J. Narboux}, Lect. Notes Comput. Sci. 7993, 89--109 (2013; Zbl 1397.03019) Full Text: DOI HAL
Huet, Gérard Preface to the special issue: Interactive theorem proving and the formalization of mathematics. (English) Zbl 1276.03004 Math. Struct. Comput. Sci. 21, No. 4, 671-677 (2011). MSC: 03-06 68-06 03B35 68T15 PDFBibTeX XMLCite \textit{G. Huet}, Math. Struct. Comput. Sci. 21, No. 4, 671--677 (2011; Zbl 1276.03004) Full Text: DOI
Wiedijk, Freek Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics. (English) Zbl 1114.03007 J. Appl. Log. 4, No. 4, 622-645 (2006). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{F. Wiedijk}, J. Appl. Log. 4, No. 4, 622--645 (2006; Zbl 1114.03007) Full Text: DOI
Cáccamo, Mario; Winskel, Glynn A higher-order calculus for categories. (English) Zbl 1005.18001 Boulton, Richard J. (ed.) et al., Theorem proving in higher order logics. 14th international conference, TPHOLs 2001, Edinburgh, Scotland, GB, September 3-6, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2152, 136-153 (2001). MSC: 18A15 68T15 03B35 PDFBibTeX XMLCite \textit{M. Cáccamo} and \textit{G. Winskel}, Lect. Notes Comput. Sci. 2152, 136--153 (2001; Zbl 1005.18001) Full Text: Link
Viganò, Luca [Gabbay, Dov M.] Labelled non-classical logics. With a foreword by Dov M. Gabbay. (English) Zbl 1003.03001 Dordrecht: Kluwer Academic Publishers. xiv, 291 p. (2000). Reviewer: Branislav Boričić (Beograd) MSC: 03-02 03B45 03F07 68T15 03F05 03B70 PDFBibTeX XMLCite \textit{L. Viganò}, Labelled non-classical logics. With a foreword by Dov M. Gabbay. Dordrecht: Kluwer Academic Publishers (2000; Zbl 1003.03001)
McAllester, David (ed.) Automated deduction - CADE-17. 17th international conference, Pittsburgh, PA, USA, June 17–20, 2000. Proceedings. (English) Zbl 0939.00024 Lecture Notes in Computer Science 1831. Lecture Notes in Artificial Intelligence. Berlin: Springer. xiii, 519 p. (2000). MSC: 00B25 03-06 68-06 PDFBibTeX XMLCite \textit{D. McAllester} (ed.), Automated deduction - CADE-17. 17th international conference, Pittsburgh, PA, USA, June 17--20, 2000. Proceedings. Berlin: Springer (2000; Zbl 0939.00024)
Paulson, Lawrence C. Set theory for verification. II: Induction and recursion. (English) Zbl 0840.68104 J. Autom. Reasoning 15, No. 2, 167-215 (1995). MSC: 68T15 03E75 03-04 PDFBibTeX XMLCite \textit{L. C. Paulson}, J. Autom. Reasoning 15, No. 2, 167--215 (1995; Zbl 0840.68104) Full Text: DOI arXiv
Cantini, Andrea Levels of truth. (English) Zbl 0836.03033 Notre Dame J. Formal Logic 36, No. 2, 185-213 (1995). MSC: 03F35 PDFBibTeX XMLCite \textit{A. Cantini}, Notre Dame J. Formal Logic 36, No. 2, 185--213 (1995; Zbl 0836.03033) 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
Aczel, Peter; Carlisle, David P.; Mendler, Nax Two frameworks of theories and their implementation in Isabelle. (English) Zbl 0756.03013 Logical frameworks, Proc. 1st Annu. Workshop, Sophia-Antipolis/Fr. 1990, 3-39 (1991). MSC: 03B70 03F35 68T15 03B40 03-04 PDFBibTeX XMLCite \textit{P. Aczel} et al., in: Logical frameworks. Proceedings of the first annual workshop ''Logical frameworks: design, implementation and experiment'', held in Sophia- Antipolis, France, May 7-11, 1990. Cambridge etc.: Cambridge University Press. 3--39 (1991; Zbl 0756.03013)