Isabelle/HOL swMATH ID: 1569 Software Authors: Naraschewski, Wolfgang; Nipkow, Tobias Description: Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols. Homepage: http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Keywords: simply typed lambda calculus; Mini-ML; computation of the most general type; type inference algorithm; machine-checked proof of correctness and completeness Related Software: Isabelle; Coq; HOL; Archive Formal Proofs; PVS; HOL Light; Sledgehammer; Mizar; z3; ML; TPTP; Isar; ACL2; VAMPIRE; Isabelle/Isar; seL4; Nitpick; E Theorem Prover; Locales; Nominal Isabelle Cited in: 1,033 Documents Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias 2011 Type inference verified: Algorithm \({\mathcal W}\) in Isabelle/HOL. Zbl 0927.03025Naraschewski, Wolfgang; Nipkow, Tobias 1998 all top 5 Cited by 1,149 Authors 69 Nipkow, Tobias 46 Blanchette, Jasmin Christian 35 Paulson, Lawrence Charles 33 Benzmüller, Christoph Ewald 30 Popescu, Andrei 28 Thiemann, René 27 Kaliszyk, Cezary 27 Klein, Gerwin 25 Lochbihler, Andreas 25 Sternagel, Christian 23 Traytel, Dmitry 21 Struth, Georg 18 Lammich, Peter 17 Urban, Christian 16 Foster, Simon 16 Urban, Josef 15 Hölzl, Johannes 14 Guttmann, Walter 14 Weber, Tjark 13 Krauss, Alexander 12 Rabe, Florian 12 Wenzel, Makarius 11 Böhme, Sascha 11 Wolff, Burkhart 10 Berghofer, Stefan 10 Woodcock, James C. P. 9 Avigad, Jeremy 9 Coghetto, Roland 9 Marić, Filip 9 Preoteasa, Viorel 9 Yamada, Akihisa 8 Dawson, Jeremy E. 8 Divasón, Jose 8 Höfner, Peter 8 Immler, Fabian 8 Kammüller, Florian 8 Kunčar, Ondřej 8 Tiu, Alwen Fernanto 7 Barrett, Clark W. 7 Brucker, Achim D. 7 Eberl, Manuel 7 Fleury, Mathias 7 Kohlhase, Michael 7 Middeldorp, Aart 7 Myreen, Magnus O. 7 Norrish, Michael 7 Parrow, Joachim 7 Reynolds, Andrew 7 Tinelli, Cesare 7 Waldmann, Uwe 6 Aransay, Jesús 6 Armstrong, Alasdair 6 Basin, David A. 6 Bengtson, Jesper 6 Berghammer, Rudolf 6 Boldo, Sylvie 6 Brown, Chad Edward 6 Bulwahn, Lukas 6 Fleuriot, Jacques D. 6 Gauthier, Thibault 6 Goré, Rajeev Prabhakar 6 Haftmann, Florian 6 Hayes, Ian J. 6 Kumar, Ramana 6 Li, Yongjian 6 Melquiond, Guillaume 6 Merz, Stephan 6 Miller, Dale Allen 6 Momigliano, Alberto 6 Murray, Toby 6 Schlichtkrull, Anders 6 Steen, Alexander 6 Stucke, Insa 6 Woltzenlogel Paleo, Bruno 6 Zhang, Xingyuan 5 Aspinall, David 5 Ayala-Rincón, Mauricio 5 Bentkamp, Alexander 5 Beringer, Lennart 5 Brockschmidt, Marc 5 Cavalcanti, Ana 5 Chaieb, Amine 5 Giesl, Jürgen 5 Haslbeck, Max W. 5 Haslbeck, Maximilian P. L. 5 Huerta y Munive, Jonathan Julián 5 Huffman, Brian 5 Joosten, Sebastiaan J. C. 5 Koutsoukou-Argyraki, Angeliki 5 Li, Wenda 5 Mayero, Micaela 5 Mossakowski, Till 5 Nagashima, Yutaka 5 Nieto, Leonor Prensa 5 Pąk, Karol 5 Pang, Jun 5 Platzer, André 5 Schneider-Kamp, Peter 5 Schneider, Joshua P. 5 Sewell, Thomas D. ...and 1,049 more Authors all top 5 Cited in 70 Serials 142 Journal of Automated Reasoning 29 Formal Aspects of Computing 17 Journal of Logical and Algebraic Methods in Programming 16 Theoretical Computer Science 16 Logical Methods in Computer Science 11 Formalized Mathematics 10 Journal of Symbolic Computation 10 Lecture Notes in Computer Science 8 Information and Computation 8 ACM Transactions on Computational Logic 7 MSCS. Mathematical Structures in Computer Science 7 Formal Methods in System Design 7 Journal of Functional Programming 7 Annals of Mathematics and Artificial Intelligence 7 Journal of Formalized Reasoning 6 Journal of Applied Logic 4 Experimental Mathematics 4 Fundamenta Informaticae 4 Journal of Applied Mathematics 4 Mathematics in Computer Science 3 The Journal of Logic and Algebraic Programming 3 Logica Universalis 2 Acta Informatica 2 Artificial Intelligence 2 Information Processing Letters 2 Studia Logica 2 Science of Computer Programming 2 International Journal of Foundations of Computer Science 2 Journal of Applied Non-Classical Logics 2 Nordic Journal of Computing 2 Journal of the ACM 2 Concurrency and Computation: Practice & Experience 2 Scientific Annals of Computer Science 2 The Review of Symbolic Logic 1 ACM Computing Surveys 1 International Journal of General Systems 1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) 1 Journal of Economic Theory 1 Journal of Functional Analysis 1 Journal of the Korean Mathematical Society 1 Programming and Computer Software 1 Synthese 1 Bulletin of the Section of Logic 1 Discrete & Computational Geometry 1 SIAM Journal on Discrete Mathematics 1 Journal of Cryptology 1 AI Communications 1 Journal of Logic and Computation 1 International Journal of Computer Mathematics 1 Distributed Computing 1 Indagationes Mathematicae. New Series 1 Applicable Algebra in Engineering, Communication and Computing 1 Computational Optimization and Applications 1 Bulletin of the Belgian Mathematical Society - Simon Stevin 1 The Bulletin of Symbolic Logic 1 Logic Journal of the IGPL 1 Wuhan University Journal of Natural Sciences (WUJNS) 1 Logic and Logical Philosophy 1 Theory and Practice of Logic Programming 1 Sādhanā 1 Computer Languages, Systems & Structures 1 SIGMA. Symmetry, Integrability and Geometry: Methods and Applications 1 Electronic Notes in Theoretical Computer Science 1 Frontiers of Computer Science in China 1 Forum of Mathematics, Pi 1 Computer Science Review 1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 Texts in Computer Science 1 Texts in Logic and Reasoning 1 Journal of Applied Logics - IfCoLog Journal of Logics and their Applications all top 5 Cited in 43 Fields 994 Computer science (68-XX) 284 Mathematical logic and foundations (03-XX) 23 Combinatorics (05-XX) 18 Information and communication theory, circuits (94-XX) 15 General and overarching topics; collections (00-XX) 14 Number theory (11-XX) 13 Numerical analysis (65-XX) 13 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 12 Real functions (26-XX) 10 Geometry (51-XX) 9 Commutative algebra (13-XX) 9 Ordinary differential equations (34-XX) 8 Category theory; homological algebra (18-XX) 7 Order, lattices, ordered algebraic structures (06-XX) 7 Linear and multilinear algebra; matrix theory (15-XX) 7 Operations research, mathematical programming (90-XX) 7 Systems theory; control (93-XX) 5 Convex and discrete geometry (52-XX) 5 Probability theory and stochastic processes (60-XX) 4 General algebraic systems (08-XX) 4 Field theory and polynomials (12-XX) 4 Dynamical systems and ergodic theory (37-XX) 4 Relativity and gravitational theory (83-XX) 3 Group theory and generalizations (20-XX) 3 Topological groups, Lie groups (22-XX) 3 Functions of a complex variable (30-XX) 3 Partial differential equations (35-XX) 3 Algebraic topology (55-XX) 2 Algebraic geometry (14-XX) 2 General topology (54-XX) 2 Mechanics of particles and systems (70-XX) 2 Biology and other natural sciences (92-XX) 2 Mathematics education (97-XX) 1 History and biography (01-XX) 1 Measure and integration (28-XX) 1 Several complex variables and analytic spaces (32-XX) 1 Special functions (33-XX) 1 Functional analysis (46-XX) 1 Differential geometry (53-XX) 1 Manifolds and cell complexes (57-XX) 1 Fluid mechanics (76-XX) 1 Optics, electromagnetic theory (78-XX) 1 Quantum theory (81-XX) Citations by Year