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: Coq; Isabelle; HOL; Archive Formal Proofs; HOL Light; PVS; Sledgehammer; Mizar; z3; ML; Isar; Nominal Isabelle; ACL2; TPTP; VAMPIRE; GitHub; E Theorem Prover; Nitpick; seL4; Isabelle/Isar Cited in: 1,433 Documents Standard Articles 3 Publications describing the Software, including 3 Publications in zbMATH Year Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias 2011 Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus 2002 Type inference verified: Algorithm \({\mathcal W}\) in Isabelle/HOL. Zbl 0927.03025Naraschewski, Wolfgang; Nipkow, Tobias 1998 all top 5 Cited by 1,641 Authors 77 Nipkow, Tobias 49 Blanchette, Jasmin Christian 41 Benzmüller, Christoph Ewald 41 Paulson, Lawrence Charles 33 Kaliszyk, Cezary 30 Popescu, Andrei 28 Thiemann, René 27 Klein, Gerwin 26 Lochbihler, Andreas 26 Traytel, Dmitry 25 Sternagel, Christian 25 Urban, Josef 24 Struth, Georg 22 Lammich, Peter 21 Foster, Simon 18 Urban, Christian 17 Weber, Tjark 16 Hölzl, Johannes 15 Rabe, Florian 14 Guttmann, Walter 14 Wenzel, Makarius 14 Wolff, Burkhart 13 Krauss, Alexander 13 Tahar, Sofiène 13 Woodcock, James C. P. 12 Hasan, Osman 11 Berghofer, Stefan 11 Böhme, Sascha 11 Kammüller, Florian 11 Norrish, Michael 10 Avigad, Jeremy 10 Coghetto, Roland 10 Myreen, Magnus O. 10 Parrow, Joachim 10 Tinelli, Cesare 9 Ayala-Rincón, Mauricio 9 Barrett, Clark W. 9 Brucker, Achim D. 9 Divasón, Jose 9 Dongol, Brijesh 9 Fleuriot, Jacques D. 9 Fleury, Mathias 9 Höfner, Peter 9 Immler, Fabian 9 Kohlhase, Michael 9 Marić, Filip 9 Platzer, André 9 Preoteasa, Viorel 9 Yamada, Akihisa 9 Zhan, Bohua 8 Aransay, Jesús 8 Basin, David A. 8 Berghammer, Rudolf 8 Cavalcanti, Ana 8 Dawson, Jeremy E. 8 de Boer, Frank S. 8 Eberl, Manuel 8 Fuenmayor, David 8 Gauthier, Thibault 8 Hayes, Ian J. 8 Janičić, Predrag 8 Kumar, Ramana 8 Kunčar, Ondřej 8 Miller, Dale Allen 8 Mossakowski, Till 8 Murray, Toby 8 Reynolds, Andrew 8 Schlichtkrull, Anders 8 Steen, Alexander 8 Tiu, Alwen Fernanto 8 Waldmann, Uwe 7 Bengtson, Jesper 7 Boldo, Sylvie 7 Cheney, James 7 Goré, Rajeev Prabhakar 7 Haftmann, Florian 7 Haslbeck, Maximilian P. L. 7 Jakubův, Jan 7 Johansson, Moa 7 Mayero, Micaela 7 Middeldorp, Aart 7 Momigliano, Alberto 7 Stucke, Insa 7 Théry, Laurent 7 Weidenbach, Christoph 7 Woltzenlogel Paleo, Bruno 6 Åman Pohjola, Johannes 6 Armstrong, Alasdair 6 Aspinall, David 6 Bentkamp, Alexander 6 Beringer, Lennart 6 Brown, Chad Edward 6 Bulwahn, Lukas 6 Colvin, Robert J. 6 From, Asta Halkjær 6 Guan, Yong 6 Joosten, Sebastiaan J. C. 6 Kaufmann, Matt 6 Li, Yongjian 6 Melquiond, Guillaume ...and 1,541 more Authors all top 5 Cited in 93 Serials 182 Journal of Automated Reasoning 47 Formal Aspects of Computing 36 Theoretical Computer Science 25 Logical Methods in Computer Science 22 Journal of Logical and Algebraic Methods in Programming 17 Formalized Mathematics 13 Journal of Functional Programming 12 Journal of Symbolic Computation 12 Mathematical Structures in Computer Science 12 Formal Methods in System Design 11 Annals of Mathematics and Artificial Intelligence 10 Information and Computation 10 Lecture Notes in Computer Science 9 ACM Transactions on Computational Logic 9 Journal of Applied Logic 8 Journal of Formalized Reasoning 6 Mathematics in Computer Science 5 Science of Computer Programming 5 The Journal of Logic and Algebraic Programming 4 Experimental Mathematics 4 Fundamenta Informaticae 4 Concurrency and Computation: Practice & Experience 4 Journal of Applied Mathematics 4 The Review of Symbolic Logic 4 Journal of Applied Logics - IfCoLog Journal of Logics and their Applications 3 Acta Informatica 3 Annals of Pure and Applied Logic 3 International Journal of Foundations of Computer Science 3 Theory and Practice of Logic Programming 3 Sādhanā 3 Logica Universalis 2 Artificial Intelligence 2 Information Processing Letters 2 Programming and Computer Software 2 Studia Logica 2 Synthese 2 AI Communications 2 Journal of Logic and Computation 2 Journal of Applied Non-Classical Logics 2 Nordic Journal of Computing 2 Journal of the ACM 2 Higher-Order and Symbolic Computation 2 Scientific Annals of Computer Science 2 Frontiers of Computer Science 1 ACM Computing Surveys 1 Discrete Mathematics 1 International Journal of General Systems 1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) 1 Journal of Mathematical Physics 1 Chaos, Solitons and Fractals 1 Automatica 1 Information Sciences 1 Journal of Combinatorial Theory. Series A 1 Journal of Computer and System Sciences 1 Journal of Economic Theory 1 Journal of Functional Analysis 1 Journal of the Korean Mathematical Society 1 Journal of Mathematical Economics 1 Journal of Philosophical Logic 1 Software. Practice & Experience 1 Bulletin of the Section of Logic 1 Journal of Computer Science and Technology 1 Discrete & Computational Geometry 1 International Journal of Approximate Reasoning 1 SIAM Journal on Discrete Mathematics 1 Journal of Cryptology 1 Discrete Event Dynamic Systems 1 International Journal of Computer Mathematics 1 Bulletin of the American Mathematical Society. New Series 1 Distributed Computing 1 Indagationes Mathematicae. New Series 1 Applicable Algebra in Engineering, Communication and Computing 1 Computational Optimization and Applications 1 Journal of Logic, Language and Information 1 Bulletin of the Belgian Mathematical Society - Simon Stevin 1 The Bulletin of Symbolic Logic 1 Theory of Computing Systems 1 Logic Journal of the IGPL 1 Soft Computing 1 Wuhan University Journal of Natural Sciences (WUJNS) 1 Logic and Logical Philosophy 1 Computer Languages, Systems & Structures 1 SIGMA. Symmetry, Integrability and Geometry: Methods and Applications 1 Electronic Notes in Theoretical Computer Science 1 Nonlinear Analysis. Hybrid Systems 1 Numerical Algebra, Control and Optimization 1 Frontiers of Computer Science in China 1 Forum of Mathematics, Pi 1 Computer Science Review 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 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 all top 5 Cited in 46 Fields 1,372 Computer science (68-XX) 399 Mathematical logic and foundations (03-XX) 28 Combinatorics (05-XX) 26 Information and communication theory, circuits (94-XX) 19 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 18 General and overarching topics; collections (00-XX) 18 Number theory (11-XX) 17 Real functions (26-XX) 17 Numerical analysis (65-XX) 16 Systems theory; control (93-XX) 15 Category theory; homological algebra (18-XX) 14 Geometry (51-XX) 11 Commutative algebra (13-XX) 11 Linear and multilinear algebra; matrix theory (15-XX) 11 Operations research, mathematical programming (90-XX) 10 Ordinary differential equations (34-XX) 8 Order, lattices, ordered algebraic structures (06-XX) 7 Probability theory and stochastic processes (60-XX) 6 Field theory and polynomials (12-XX) 6 Group theory and generalizations (20-XX) 6 Convex and discrete geometry (52-XX) 6 Relativity and gravitational theory (83-XX) 5 General algebraic systems (08-XX) 5 Measure and integration (28-XX) 5 Dynamical systems and ergodic theory (37-XX) 5 General topology (54-XX) 5 Quantum theory (81-XX) 4 Algebraic topology (55-XX) 4 Mathematics education (97-XX) 3 History and biography (01-XX) 3 Topological groups, Lie groups (22-XX) 3 Functions of a complex variable (30-XX) 3 Partial differential equations (35-XX) 3 Mechanics of particles and systems (70-XX) 3 Optics, electromagnetic theory (78-XX) 3 Biology and other natural sciences (92-XX) 2 Algebraic geometry (14-XX) 2 Associative rings and algebras (16-XX) 1 Several complex variables and analytic spaces (32-XX) 1 Special functions (33-XX) 1 Functional analysis (46-XX) 1 Calculus of variations and optimal control; optimization (49-XX) 1 Differential geometry (53-XX) 1 Manifolds and cell complexes (57-XX) 1 Fluid mechanics (76-XX) 1 Geophysics (86-XX) Citations by Year