×

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; E Theorem Prover; seL4; Nitpick; Haskell; CeTA
Referenced in: 972 Publications
all top 5

Referenced by 1,082 Authors

64 Nipkow, Tobias
44 Blanchette, Jasmin Christian
33 Benzmüller, Christoph Ewald
33 Paulson, Lawrence Charles
29 Popescu, Andrei
27 Klein, Gerwin
27 Thiemann, René
25 Kaliszyk, Cezary
25 Sternagel, Christian
23 Lochbihler, Andreas
21 Struth, Georg
21 Traytel, Dmitry
17 Urban, Christian
16 Lammich, Peter
15 Foster, Simon
15 Hölzl, Johannes
15 Urban, Josef
14 Weber, Tjark
13 Krauss, Alexander
12 Guttmann, Walter
12 Rabe, Florian
11 Böhme, Sascha
11 Wenzel, Makarius
11 Wolff, Burkhart
10 Berghofer, Stefan
9 Coghetto, Roland
9 Marić, Filip
9 Preoteasa, Viorel
9 Woodcock, James C. P.
8 Avigad, Jeremy
8 Dawson, Jeremy E.
8 Höfner, Peter
8 Kammüller, Florian
8 Kunčar, Ondřej
8 Tiu, Alwen Fernanto
8 Yamada, Akihisa
7 Brucker, Achim D.
7 Divasón, Jose
7 Eberl, Manuel
7 Fleury, Mathias
7 Immler, Fabian
7 Kohlhase, Michael
7 Murray, Toby
7 Myreen, Magnus O.
7 Norrish, Michael
7 Parrow, Joachim
6 Aransay, Jesús
6 Armstrong, Alasdair
6 Barrett, Clark W.
6 Bengtson, Jesper
6 Berghammer, Rudolf
6 Boldo, Sylvie
6 Bulwahn, Lukas
6 Gauthier, Thibault
6 Goré, Rajeev Prabhakar
6 Haftmann, Florian
6 Kumar, Ramana
6 Li, Yongjian
6 Melquiond, Guillaume
6 Middeldorp, Aart
6 Miller, Dale Allen
6 Momigliano, Alberto
6 Reynolds, Andrew
6 Steen, Alexander
6 Stucke, Insa
6 Tinelli, Cesare
6 Waldmann, Uwe
6 Woltzenlogel Paleo, Bruno
6 Zhang, Xingyuan
5 Aspinall, David
5 Basin, David A.
5 Beringer, Lennart
5 Brockschmidt, Marc
5 Brown, Chad Edward
5 Cavalcanti, Ana
5 Chaieb, Amine
5 Giesl, Jürgen
5 Haslbeck, Max W.
5 Haslbeck, Maximilian P. L.
5 Hayes, Ian J.
5 Huffman, Brian
5 Joosten, Sebastiaan J. C.
5 Li, Wenda
5 Mayero, Micaela
5 Mossakowski, Till
5 Nagashima, Yutaka
5 Nieto, Leonor Prensa
5 Pang, Jun
5 Platzer, André
5 Schlichtkrull, Anders
5 Schneider-Kamp, Peter
5 Sewell, Thomas D.
5 Strecker, Martin
5 von Oheimb, David
5 Zeyda, Frank
5 Zhan, Bohua
4 Andronick, June
4 Ayala-Rincón, Mauricio
4 Bauer, Gertrud
4 Bentkamp, Alexander
...and 982 more Authors
all top 5

Referenced in 67 Serials

129 Journal of Automated Reasoning
29 Formal Aspects of Computing
16 Journal of Logical and Algebraic Methods in Programming
15 Theoretical Computer Science
14 Logical Methods in Computer Science
11 Formalized Mathematics
10 Journal of Symbolic Computation
10 Lecture Notes in Computer Science
8 Information and Computation
8 Journal of Functional Programming
8 ACM Transactions on Computational Logic
7 MSCS. Mathematical Structures in Computer Science
7 Formal Methods in System Design
7 Annals of Mathematics and Artificial Intelligence
7 Journal of Formalized Reasoning
6 Journal of Applied Logic
4 Experimental Mathematics
4 Journal of Applied Mathematics
4 Mathematics in Computer Science
3 Fundamenta Informaticae
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 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 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 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 Journal of the ACM
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
all top 5

Referenced in 43 Fields

935 Computer science (68-XX)
266 Mathematical logic and foundations (03-XX)
21 Combinatorics (05-XX)
17 Information and communication theory, circuits (94-XX)
15 General and overarching topics; collections (00-XX)
13 Numerical analysis (65-XX)
12 Real functions (26-XX)
10 Number theory (11-XX)
10 Geometry (51-XX)
10 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
9 Ordinary differential equations (34-XX)
7 Order, lattices, ordered algebraic structures (06-XX)
7 Commutative algebra (13-XX)
7 Category theory; homological algebra (18-XX)
7 Systems theory; control (93-XX)
6 Linear and multilinear algebra; matrix theory (15-XX)
6 Operations research, mathematical programming (90-XX)
5 Convex and discrete geometry (52-XX)
4 General algebraic systems (08-XX)
4 Field theory and polynomials (12-XX)
4 Dynamical systems and ergodic theory (37-XX)
4 Probability theory and stochastic processes (60-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 Group theory and generalizations (20-XX)
2 General topology (54-XX)
2 Mechanics of particles and systems (70-XX)
2 Relativity and gravitational theory (83-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)

Referencing Publications by Year