Xu, Runqing; Li, Liming; Zhan, Bohua Verified interactive computation of definite integrals. (English) Zbl 07437096 Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 485-503 (2021). MSC: 03B35 68V15 PDF BibTeX XML Cite \textit{R. Xu} et al., Lect. Notes Comput. Sci. 12699, 485--503 (2021; Zbl 07437096) Full Text: DOI OpenURL
Reiche, Sebastian; Benzmüller, Christoph Public announcement logic in HOL. (English) Zbl 07437025 Martins, Manuel A. (ed.) et al., Dynamic logic. New trends and applications. Third international workshop, Dalí 2020, Prague, Czech Republic, October 9–10, 2020. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 12569, 222-238 (2020). MSC: 03B42 68V15 PDF BibTeX XML Cite \textit{S. Reiche} and \textit{C. Benzmüller}, Lect. Notes Comput. Sci. 12569, 222--238 (2020; Zbl 07437025) Full Text: DOI arXiv OpenURL
Kohl, Christina; Middeldorp, Aart Composing proof terms. (English) Zbl 07178985 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 337-353 (2019). MSC: 03B35 68V15 PDF BibTeX XML Cite \textit{C. Kohl} and \textit{A. Middeldorp}, Lect. Notes Comput. Sci. 11716, 337--353 (2019; Zbl 07178985) Full Text: DOI OpenURL
Czajka, Łukasz; Kaliszyk, Cezary Hammer for Coq: automation for dependent type theory. (English) Zbl 1448.68458 J. Autom. Reasoning 61, No. 1-4, 423-453 (2018). MSC: 68V15 03B35 PDF BibTeX XML Cite \textit{Ł. Czajka} and \textit{C. Kaliszyk}, J. Autom. Reasoning 61, No. 1--4, 423--453 (2018; Zbl 1448.68458) Full Text: DOI OpenURL
Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W. VST-Floyd: a separation logic tool to verify correctness of C programs. (English) Zbl 1451.68169 J. Autom. Reasoning 61, No. 1-4, 367-422 (2018). MSC: 68Q60 03B70 68V15 PDF BibTeX XML Cite \textit{Q. Cao} et al., J. Autom. Reasoning 61, No. 1--4, 367--422 (2018; Zbl 1451.68169) Full Text: DOI OpenURL
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef TacticToe: learning to reason with HOL4 tactics. (English) Zbl 1403.68224 Eiter, Thomas (ed.) et al., LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers. Manchester: EasyChair. EPiC Series in Computing 46, 15-143 (2017). MSC: 68T15 68T05 PDF BibTeX XML Cite \textit{T. Gauthier} et al., EPiC Ser. Comput. 46, 15--143 (2017; Zbl 1403.68224) Full Text: DOI arXiv OpenURL
Slama, Franck; Brady, Edwin Automatically proving equivalence by type-safe reflection. (English) Zbl 1367.68257 Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 40-55 (2017). MSC: 68T15 68N30 PDF BibTeX XML Cite \textit{F. Slama} and \textit{E. Brady}, Lect. Notes Comput. Sci. 10383, 40--55 (2017; Zbl 1367.68257) Full Text: DOI Link OpenURL
Matichuk, Daniel; Murray, Toby; Wenzel, Makarius Eisbach: a proof method language for Isabelle. (English) Zbl 1356.68195 J. Autom. Reasoning 56, No. 3, 261-282 (2016). MSC: 68T15 PDF BibTeX XML Cite \textit{D. Matichuk} et al., J. Autom. Reasoning 56, No. 3, 261--282 (2016; Zbl 1356.68195) Full Text: DOI OpenURL
Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev SEPIA: search for proofs using inferred automata. (English) Zbl 1465.68284 Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 246-255 (2015). MSC: 68V15 PDF BibTeX XML Cite \textit{T. Gransden} et al., Lect. Notes Comput. Sci. 9195, 246--255 (2015; Zbl 1465.68284) Full Text: DOI arXiv OpenURL
Zeyda, Frank; Cavalcanti, Ana Laws of mission-based programming. (English) Zbl 1331.68054 Formal Asp. Comput. 27, No. 2, 423-472 (2015). MSC: 68N30 68N19 PDF BibTeX XML Cite \textit{F. Zeyda} and \textit{A. Cavalcanti}, Formal Asp. Comput. 27, No. 2, 423--472 (2015; Zbl 1331.68054) Full Text: DOI Link OpenURL
Preoteasa, Viorel; Back, Ralph-Johan; Eriksson, Johannes Verification and code generation for invariant diagrams in Isabelle. (English) Zbl 1304.68032 J. Log. Algebr. Methods Program. 84, No. 1, 19-36 (2015). MSC: 68N30 68Q60 68T15 PDF BibTeX XML Cite \textit{V. Preoteasa} et al., J. Log. Algebr. Methods Program. 84, No. 1, 19--36 (2015; Zbl 1304.68032) Full Text: DOI OpenURL
Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor Mtac: a monad for typed tactic programming in Coq. (English) Zbl 1323.68236 Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP ’13, Boston, MA, USA, September 25–27, 2013. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2326-0). ACM SIGPLAN Notices 48, No. 9, 87-100 (2013). MSC: 68N30 68T15 PDF BibTeX XML Cite \textit{B. Ziliani} et al., in: Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP '13, Boston, MA, USA, September 25--27, 2013. New York, NY: Association for Computing Machinery (ACM). 87--100 (2013; Zbl 1323.68236) Full Text: DOI OpenURL
Doherty, Simon; Groves, Lindsay; Luchangco, Victor; Moir, Mark Towards formally specifying and verifying transactional memory. (English) Zbl 1298.68168 Formal Asp. Comput. 25, No. 5, 769-799 (2013). MSC: 68Q60 68N30 PDF BibTeX XML Cite \textit{S. Doherty} et al., Formal Asp. Comput. 25, No. 5, 769--799 (2013; Zbl 1298.68168) Full Text: DOI OpenURL
Gonthier, Georges; Ziliani, Beta; Nanevski, Aleksandar; Dreyer, Derek How to make ad hoc proof automation less ad hoc. (English) Zbl 1314.68281 J. Funct. Program. 23, No. 4, 357-401 (2013). Reviewer: Temur Kutsia (Linz) MSC: 68T15 68N18 PDF BibTeX XML Cite \textit{G. Gonthier} et al., J. Funct. Program. 23, No. 4, 357--401 (2013; Zbl 1314.68281) Full Text: DOI OpenURL
Benzmüller, Christoph; Paulson, Lawrence C. Quantified multimodal logics in simple type theory. (English) Zbl 1334.03014 Log. Univers. 7, No. 1, 7-20 (2013). MSC: 03B45 03B15 PDF BibTeX XML Cite \textit{C. Benzmüller} and \textit{L. C. Paulson}, Log. Univers. 7, No. 1, 7--20 (2013; Zbl 1334.03014) Full Text: DOI Link OpenURL
Myreen, Magnus O.; Gordon, Michael J. C. Function extraction. (English) Zbl 1243.68139 Sci. Comput. Program. 77, No. 4, 505-517 (2012). MSC: 68N15 68Q60 68T15 68N20 PDF BibTeX XML Cite \textit{M. O. Myreen} and \textit{M. J. C. Gordon}, Sci. Comput. Program. 77, No. 4, 505--517 (2012; Zbl 1243.68139) Full Text: DOI OpenURL
Gonthier, Georges; Ziliani, Beta; Nanevski, Aleksandar; Dreyer, Derek How to make ad hoc proof automation less ad hoc. (English) Zbl 1323.68117 Proceedings of the 16th ACM SIGPLAN international conference on functional programming, ICFP ’11, Tokyo, Japan, September 19–21, 2011. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-0865-6). ACM SIGPLAN Notices 46, No. 9, 163-175 (2011). MSC: 68N18 68T15 PDF BibTeX XML Cite \textit{G. Gonthier} et al., in: Proceedings of the 16th ACM SIGPLAN international conference on functional programming, ICFP '11, Tokyo, Japan, September 19--21, 2011. New York, NY: Association for Computing Machinery (ACM). 163--175 (2011; Zbl 1323.68117) Full Text: DOI Link OpenURL
Contejean, Évelyne; Courtieu, Pierre; Forest, Julien; Pons, Olivier; Urbain, Xavier Automated certified proofs with CiME3. (English) Zbl 1236.68219 Schmid-Schauß, Manfred (ed.), 22nd international conference on rewriting techniques and applications (RTA 2011), Novi Sad, Serbia, May 30 – June 1, 2011. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-30-9). LIPIcs – Leibniz International Proceedings in Informatics 10, 21-30, electronic only (2011). MSC: 68T15 68Q42 PDF BibTeX XML Cite \textit{É. Contejean} et al., LIPIcs -- Leibniz Int. Proc. Inform. 10, 21--30 (2011; Zbl 1236.68219) Full Text: DOI Link OpenURL
Génevaux, Jean-David; Narboux, Julien; Schreck, Pascal Formalization of Wu’s simple method in Coq. (English) Zbl 1350.68234 Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 71-86 (2011). MSC: 68T15 PDF BibTeX XML Cite \textit{J.-D. Génevaux} et al., Lect. Notes Comput. Sci. 7086, 71--86 (2011; Zbl 1350.68234) Full Text: DOI Link OpenURL
Chlipala, Adam An introduction to programming and proving with dependent types in Coq. (English) Zbl 1211.68367 J. Formaliz. Reason. 3, No. 2, 1-93 (2010). MSC: 68T15 PDF BibTeX XML Cite \textit{A. Chlipala}, J. Formaliz. Reason. 3, No. 2, 1--93 (2010; Zbl 1211.68367) Full Text: Link OpenURL
Benzmüller, Christoph E.; Brown, Chad E.; Kohlhase, Michael Cut-simulation and impredicativity. (English) Zbl 1160.03004 Log. Methods Comput. Sci. 5, No. 1, Paper 8, 21 p. (2009). MSC: 03B35 03B15 03F05 PDF BibTeX XML Cite \textit{C. E. Benzmüller} et al., Log. Methods Comput. Sci. 5, No. 1, Paper 8, 21 p. (2009; Zbl 1160.03004) Full Text: DOI arXiv OpenURL
Benzmüller, Christoph E.; Brown, Chad E.; Kohlhase, Michael Cut-simulation in impredicative logics. (English) Zbl 1159.03303 Furbach, Ulrich (ed.) et al., Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17–20, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37187-8/pbk). Lecture Notes in Computer Science 4130. Lecture Notes in Artificial Intelligence, 220-234 (2006). MSC: 03B35 03B15 03F05 PDF BibTeX XML Cite \textit{C. E. Benzmüller} et al., Lect. Notes Comput. Sci. 4130, 220--234 (2006; Zbl 1159.03303) Full Text: DOI OpenURL
Bertini, Marc; Lönnblad, Leif; Sjöstrand, Torbjörn PYTHIA version 7-0. 0 – a proof-of-concept version. (English) Zbl 0991.81011 Comput. Phys. Commun. 134, No. 3, 365-391 (2001). Reviewer: Vladimir N.Grebenev (Novosibirsk) MSC: 81-04 81-08 PDF BibTeX XML Cite \textit{M. Bertini} et al., Comput. Phys. Commun. 134, No. 3, 365--391 (2001; Zbl 0991.81011) Full Text: DOI arXiv OpenURL
Kabulov, V. K.; Tolok, V. A. The limit points definition on given topological space \((X,T)\) on finite set. (Russian) Zbl 0984.68756 Vopr. Vychisl. Prikl. Mat. 103, 4-10 (1997). Reviewer: Valery Karachik (Tashkent) MSC: 68W30 68T15 03E30 03F07 68W05 PDF BibTeX XML Cite \textit{V. K. Kabulov} and \textit{V. A. Tolok}, Vopr. Vychisl. Prikl. Mat. 103, 4--10 (1997; Zbl 0984.68756) OpenURL