Edit Profile (opens in new tab) Nipkow, Tobias Co-Author Distance Author ID: nipkow.tobias Published as: Nipkow, Tobias External Links: MGP · Wikidata · dblp · GND · IdRef Documents Indexed: 109 Publications since 1982, including 3 Books 8 Contributions as Editor Biographic References: 2 Publications Co-Authors: 87 Co-Authors with 87 Joint Publications 1,360 Co-Co-Authors all top 5 Co-Authors 30 single-authored 6 Hölzl, Johannes 5 Haslbeck, Maximilian P. L. 4 Eberl, Manuel 4 Haftmann, Florian 4 Klein, Gerwin 4 Martin, Ursula 4 Paulson, Lawrence Charles 4 Popescu, Andrei 3 Bauer, Gertrud 3 Berghofer, Stefan 3 Blanchette, Jasmin Christian 3 Krauss, Alexander 3 Obua, Steven 3 Prehofer, Christian 3 Qian, Zhenyu 3 Traytel, Dmitry 3 von Oheimb, David 3 Wenzel, Makarius 3 Wildmoser, Martin 2 Aehlig, Klaus 2 Bulwahn, Lukas 2 Chaieb, Amine 2 Eßmann, Robin 2 Hales, Thomas Callister 2 Haslbeck, Max W. 2 McLaughlin, Sean 2 Mehta, Farhad 2 Merz, Stephan 2 Naraschewski, Wolfgang 2 Robillard, Simon 2 Roßkopf, Simon 2 Urban, Christian 2 Zumkeller, Roland 1 Abdulaziz, Mohammad 1 Adams, Mark 1 Autexier, Serge 1 Baader, Franz 1 Barendregt, Hendrik Pieter 1 Böhme, Sascha 1 Brinkop, Hauke 1 Broy, Manfred 1 Dang, Tat Dat 1 Goré, Rajeev Prabhakar 1 Heering, Jan 1 Hinkel, Ursula 1 Hoàng Lê Trường 1 Hu, Shuwei 1 Hupel, Lars 1 Jiang, Dongchen 1 Kaliszyk, Cezary 1 Kunčar, Ondřej 1 Lammich, Peter 1 Leitsch, Alexander 1 Magron, Victor 1 Mantel, Heiko 1 Matichuk, Daniel 1 Mayr, Richard M. 1 Mehlhorn, Kurt 1 Meinke, Karl 1 Michaelis, Julius 1 Misra, Jayadev 1 Möller, Bernhard 1 Mueller, Olaf 1 Mündler, Niels 1 Nanz, Sebastian 1 Nguyen, Quang Truong 1 Nguyen, Tat Thang 1 Pleso, Joseph 1 Pusch, Cornelia 1 Rau, Martin 1 Rute, Jason 1 Schieder, Birgit 1 Schultz, Paula 1 Sekerinski, Emil 1 Slind, Konrad 1 Slotosch, Oscar 1 Solovyev, Alexey 1 Stevens, Lukas 1 Sulejmani, Ujkan 1 Tạ Thị Hoài An 1 Tran, Nam Trung 1 Trieu, Thi Diep 1 Urban, Josef 1 Vu, Ky Khac 1 Weikum, Gerhard 1 Wenzel, Markus 1 Wimmer, Simon all top 5 Serials 12 Journal of Automated Reasoning 7 Lecture Notes in Computer Science 4 Journal of Functional Programming 3 Formal Aspects of Computing 2 Theoretical Computer Science 2 Journal of Symbolic Computation 1 Acta Informatica 1 Journal of the Association for Computing Machinery 1 Science of Computer Programming 1 Discrete & Computational Geometry 1 Information and Computation 1 Annals of Mathematics and Artificial Intelligence 1 Concurrency and Computation: Practice & Experience 1 Electronic Notes in Theoretical Computer Science 1 Logical Methods in Computer Science 1 Journal of Formalized Reasoning 1 Forum of Mathematics, Pi all top 5 Fields 113 Computer science (68-XX) 39 Mathematical logic and foundations (03-XX) 8 General and overarching topics; collections (00-XX) 4 Convex and discrete geometry (52-XX) 3 Combinatorics (05-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 2 General algebraic systems (08-XX) 2 Operations research, mathematical programming (90-XX) 1 Associative rings and algebras (16-XX) 1 Probability theory and stochastic processes (60-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Mathematics education (97-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 101 Publications have been cited 1,837 times in 1,285 Documents Cited by ▼ Year ▼ Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131 Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus 488 2002 Term rewriting and all that. Zbl 0948.68098 Baader, Franz; Nipkow, Tobias 350 1999 Concrete semantics. With Isabelle/HOL. Zbl 1410.68004 Nipkow, Tobias; Klein, Gerwin 63 2014 Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326 Blanchette, Jasmin Christian; Nipkow, Tobias 60 2010 Code generation via higher-order rewrite systems. Zbl 1284.68131 Haftmann, Florian; Nipkow, Tobias 50 2010 A formal proof of the Kepler conjecture. Zbl 1379.52018 Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland 44 2017 Higher-order rewrite systems and their confluence. Zbl 0895.68078 Mayr, Richard; Nipkow, Tobias 38 1998 Sledgehammer: judgement day. Zbl 1291.68327 Böhme, Sascha; Nipkow, Tobias 35 2010 The Isabelle framework. Zbl 1165.68478 Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias 28 2008 Data refinement in Isabelle/HOL. Zbl 1317.68212 Haftmann, Florian; Krauss, Alexander; Kunčar, Ondřej; Nipkow, Tobias 26 2013 Hoare logics in Isabelle/HOL. Zbl 1097.68632 Nipkow, Tobias 25 2002 Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214 Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias 25 2011 Executing higher order logic. Zbl 1054.68133 Berghofer, Stefan; Nipkow, Tobias 22 2002 Winskel is (almost) right: Towards a mechanized semantics textbook. Zbl 0910.68138 Nipkow, Tobias 20 1998 Boolean unification - the story so far. Zbl 0682.68093 Martin, Ursula; Nipkow, Tobias 19 1989 Proof Pearl: regular expression equivalence and relation algebra. Zbl 1269.68090 Krauss, Alexander; Nipkow, Tobias 19 2012 Proving pointer programs in higher-order logic. Zbl 1081.68008 Mehta, Farhad; Nipkow, Tobias 17 2005 A revision of the proof of the Kepler conjecture. Zbl 1195.52004 Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland 17 2010 Flyspeck I: Tame graphs. Zbl 1222.52018 Nipkow, Tobias; Bauer, Gertrud; Schultz, Paula 16 2006 Verified bytecode verifiers. Zbl 1038.68109 Klein, Gerwin; Nipkow, Tobias 16 2003 More Church-Rosser proofs (in Isabelle/HOL). Zbl 0958.03011 Nipkow, Tobias 15 2001 Flyspeck II: The basic linear programs. Zbl 1184.68465 Obua, Steven; Nipkow, Tobias 14 2009 Hoare logics for recursive procedures and unbounded nondeterminism. Zbl 1020.03029 Nipkow, Tobias 14 2002 Unified decision procedures for regular expression equivalence. Zbl 1416.68175 Nipkow, Tobias; Traytel, Dmitriy 13 2014 Orthogonal higher-order rewrite systems are confluent. Zbl 0789.68081 Nipkow, Tobias 13 1993 HOLCF=HOL+LCF. Zbl 0933.03028 Müller, Olaf; Nipkow, Tobias; von Oheimb, David; Slotosch, Oscar 12 1999 A decidability result about sufficient-completeness of axiomatically specified abstract data types. Zbl 0493.68024 Nipkow, Tobias; Weikum, Gerhard 12 1982 Ordered rewriting and confluence. Zbl 1509.68120 Martin, Ursula; Nipkow, Tobias 12 1990 Mining the Archive of Formal Proofs. Zbl 1417.68176 Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias 11 2015 Proof terms for simply typed higher order logic. Zbl 0974.03013 Berghofer, Stefan; Nipkow, Tobias 10 2000 A verified compiler from Isabelle/HOL to CakeML. Zbl 1418.68045 Hupel, Lars; Nipkow, Tobias 10 2018 Proof pearl: Defining functions over finite sets. Zbl 1152.68529 Nipkow, Tobias; Paulson, Lawrence C. 10 2005 Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. Zbl 1064.68543 von Oheimb, David; Nipkow, Tobias 10 2002 Combining matching algorithms: The regular case. Zbl 0767.68069 Nipkow, Tobias 10 1991 Social choice theory in HOL. Arrow and Gibbard-Satterthwaite. Zbl 1185.68631 Nipkow, Tobias 10 2009 Finding lexicographic orders for termination proofs in Isabelle/HOL. Zbl 1144.68352 Bulwahn, Lukas; Krauss, Alexander; Nipkow, Tobias 10 2007 Amortized complexity verified. Zbl 1465.68059 Nipkow, Tobias 9 2015 Unification in primal algebras, their powers and their varieties. Zbl 0711.68092 Nipkow, Tobias 9 1990 Certifying machine code safety: Shallow versus deep embedding. Zbl 1099.68545 Wildmoser, Martin; Nipkow, Tobias 9 2004 Non-deterministic data types: Models and implementations. Zbl 0564.68013 Nipkow, Tobias 9 1986 From LCF to Isabelle/HOL. Zbl 1427.68349 Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius 9 2019 Automatic functional correctness proofs for functional search trees. Zbl 1478.68065 Nipkow, Tobias 8 2016 Type reconstruction for type classes. Zbl 0833.68025 Nipkow, Tobias; Prehofer, Christian 8 1995 Linear quantifier elimination. Zbl 1165.68465 Nipkow, Tobias 8 2008 Linear quantifier elimination. Zbl 1207.68339 Nipkow, Tobias 8 2010 Structured proofs in Isar/HOL. Zbl 1023.68657 Nipkow, Tobias 8 2003 Equational reasoning in Isabelle. Zbl 0683.68081 Nipkow, Tobias 7 1989 A verified compiler for probability density functions. Zbl 1335.68037 Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias 7 2015 Higher-order unification, polymorphism, and subsorts (extended abstract). Zbl 1507.68075 Nipkow, Tobias 7 1991 Verified lightweight bytecode verification. Zbl 0997.68018 Klein, Gerwin; Nipkow, Tobias 6 2001 Are homomorphisms sufficient for behavioural implementations of deterministic and nondeterministic data types? Zbl 0616.68019 Nipkow, Tobias 6 1987 Unification in Boolean rings. Zbl 0659.68111 Martin, Ursula; Nipkow, Tobias 6 1988 Proving pointer programs in higher-order logic. Zbl 1278.68274 Mehta, Farhad; Nipkow, Tobias 6 2003 \(\mu\)Java: Embedding a programming language in a theorem prover. Zbl 0995.68019 Nipkow, Tobias; von Oheimb, David; Pusch, Cornelia 5 2000 Verified bytecode verifiers. Zbl 0978.68512 Nipkow, Tobias 5 2001 Term rewriting and beyond – theorem proving in Isabelle. Zbl 0694.68059 Nipkow, Tobias 5 1989 Unification in Boolean rings. Zbl 0643.68140 Martin, Ursula; Nipkow, Tobias 5 1986 Formalized proof systems for propositional logic. Zbl 1528.03097 Michaelis, Julius; Nipkow, Tobias 5 2018 Verifying and reflecting quantifier elimination for Presburger arithmetic. Zbl 1143.03334 Chaieb, Amine; Nipkow, Tobias 5 2005 A compiled implementation of normalization by evaluation. Zbl 1165.68442 Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias 5 2008 Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L. Zbl 0943.68150 Naraschewski, Wolfgang; Nipkow, Tobias 4 1999 Higher-order rewriting and equational reasoning. Zbl 0970.68081 Nipkow, Tobias; Prehofer, Christian 4 1998 Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Zbl 0968.00052 4 2001 Observing nondeterministic data types. Zbl 0665.68013 Nipkow, Tobias 4 1988 Teaching semantics with a proof assistant: no more LSD trip proofs. Zbl 1325.68005 Nipkow, Tobias 4 2012 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1323.68346 Traytel, Dmitriy; Nipkow, Tobias 4 2013 Verified analysis of random binary tree structures. Zbl 1468.68288 Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias 4 2018 Combining matching algorithms: the regular case. Zbl 1503.68315 Nipkow, Tobias 4 1989 Modular higher-order \(E\)-unification. Zbl 1503.68144 Nipkow, Tobias; Qian, Zhenyu 4 1991 Verified efficient enumeration of plane graphs modulo isomorphism. Zbl 1342.68298 Nipkow, Tobias 4 2011 Proof synthesis and reflection for linear arithmetic. Zbl 1171.03006 Chaieb, Amine; Nipkow, Tobias 4 2008 Verifying a hotel key card system. Zbl 1168.68542 Nipkow, Tobias 4 2006 Reduction and unification in lambda calculi with subtypes. Zbl 0925.03094 Nipkow, Tobias; Qian, Zhenyu 3 1992 Amortized complexity verified. Zbl 1465.68060 Nipkow, Tobias; Brinkop, Hauke 3 2019 Hoare logics for time bounds. A study in meta theory. Zbl 1423.68098 Haslbeck, Maximilian P. L.; Nipkow, Tobias 3 2018 Formalizing probabilistic noninterference. Zbl 1426.68287 Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 3 2013 Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Zbl 1173.68002 3 2009 Isabelle’s metalogic: formalization and proof checker. Zbl 07437074 Nipkow, Tobias; Roßkopf, Simon 3 2021 Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. Zbl 07649972 Lammich, Peter; Nipkow, Tobias 3 2019 Proving concurrent noninterference. Zbl 1383.68014 Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 3 2012 The 5 colour theorem in Isabelle/Isar. Zbl 1013.68200 Bauer, Gertrud; Nipkow, Tobias 3 2002 Verified analysis of random binary tree structures. Zbl 1468.68289 Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias 3 2020 Unification in primal algebras. Zbl 0645.68045 Nipkow, Tobias 2 1988 Higher-order algebra, logic, and term rewriting. 1st international workshop, HOA ’93, Amsterdam, the Netherlands, September 23–24, 1993. Selected papers. Zbl 0825.00070 2 1994 Prototyping proof carrying code. Zbl 1094.68015 Wildmoser, Martin; Nipkow, Tobias; Klein, Gerwin; Nanz, Sebastian 2 2004 Asserting bytecode safety. Zbl 1108.68432 Wildmoser, Martin; Nipkow, Tobias 2 2005 Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference. Zbl 1394.68083 Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 2 2013 Verifying pCTL model checking. Zbl 1352.68154 Hölzl, Johannes; Nipkow, Tobias 2 2012 Verified memoization and dynamic programming. Zbl 1511.68094 Wimmer, Simon; Hu, Shuwei; Nipkow, Tobias 2 2018 Verified root-balanced trees. Zbl 1503.68052 Nipkow, Tobias 2 2017 Nominal verification of algorithm \(W\). Zbl 1195.68118 Urban, Christian; Nipkow, Tobias 2 2009 A compiled implementation of normalisation by evaluation. Zbl 1248.68130 Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias 2 2012 Abstract interpretation of annotated commands. Zbl 1360.68762 Nipkow, Tobias 2 2012 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1420.68049 Traytel, Dmitriy; Nipkow, Tobias 1 2015 More Church-Rosser proofs (in Isabelle/HOL). Zbl 1412.68248 Nipkow, Tobias 1 1996 TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Zbl 0825.00120 1 1994 Interpreter verification for a functional language. Zbl 1044.68666 Broy, Manfred; Hinkel, Ursula; Nipkow, Tobias; Prehofer, Christian; Schieder, Birgit 1 1994 Proof pearl: the marriage theorem. Zbl 1350.68237 Jiang, Dongchen; Nipkow, Tobias 1 2011 Verified approximation algorithms. Zbl 07614677 Eßmann, Robin; Nipkow, Tobias; Robillard, Simon 1 2020 Verified textbook algorithms. A biased survey. Zbl 1517.68443 Nipkow, Tobias; Eberl, Manuel; Haslbeck, Maximilian P. L. 1 2020 Isabelle’s metalogic: formalization and proof checker. Zbl 07437074 Nipkow, Tobias; Roßkopf, Simon 3 2021 Verified analysis of random binary tree structures. Zbl 1468.68289 Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias 3 2020 Verified approximation algorithms. Zbl 07614677 Eßmann, Robin; Nipkow, Tobias; Robillard, Simon 1 2020 Verified textbook algorithms. A biased survey. Zbl 1517.68443 Nipkow, Tobias; Eberl, Manuel; Haslbeck, Maximilian P. L. 1 2020 From LCF to Isabelle/HOL. Zbl 1427.68349 Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius 9 2019 Amortized complexity verified. Zbl 1465.68060 Nipkow, Tobias; Brinkop, Hauke 3 2019 Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. Zbl 07649972 Lammich, Peter; Nipkow, Tobias 3 2019 Trustworthy graph algorithms (Invited Talk). Zbl 07561645 Abdulaziz, Mohammad; Mehlhorn, Kurt; Nipkow, Tobias 1 2019 A verified compiler from Isabelle/HOL to CakeML. Zbl 1418.68045 Hupel, Lars; Nipkow, Tobias 10 2018 Formalized proof systems for propositional logic. Zbl 1528.03097 Michaelis, Julius; Nipkow, Tobias 5 2018 Verified analysis of random binary tree structures. Zbl 1468.68288 Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias 4 2018 Hoare logics for time bounds. A study in meta theory. Zbl 1423.68098 Haslbeck, Maximilian P. L.; Nipkow, Tobias 3 2018 Verified memoization and dynamic programming. Zbl 1511.68094 Wimmer, Simon; Hu, Shuwei; Nipkow, Tobias 2 2018 A formal proof of the Kepler conjecture. Zbl 1379.52018 Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland 44 2017 Verified root-balanced trees. Zbl 1503.68052 Nipkow, Tobias 2 2017 Automatic functional correctness proofs for functional search trees. Zbl 1478.68065 Nipkow, Tobias 8 2016 Mining the Archive of Formal Proofs. Zbl 1417.68176 Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias 11 2015 Amortized complexity verified. Zbl 1465.68059 Nipkow, Tobias 9 2015 A verified compiler for probability density functions. Zbl 1335.68037 Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias 7 2015 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1420.68049 Traytel, Dmitriy; Nipkow, Tobias 1 2015 Concrete semantics. With Isabelle/HOL. Zbl 1410.68004 Nipkow, Tobias; Klein, Gerwin 63 2014 Unified decision procedures for regular expression equivalence. Zbl 1416.68175 Nipkow, Tobias; Traytel, Dmitriy 13 2014 Data refinement in Isabelle/HOL. Zbl 1317.68212 Haftmann, Florian; Krauss, Alexander; Kunčar, Ondřej; Nipkow, Tobias 26 2013 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1323.68346 Traytel, Dmitriy; Nipkow, Tobias 4 2013 Formalizing probabilistic noninterference. Zbl 1426.68287 Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 3 2013 Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference. Zbl 1394.68083 Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 2 2013 Proof Pearl: regular expression equivalence and relation algebra. Zbl 1269.68090 Krauss, Alexander; Nipkow, Tobias 19 2012 Teaching semantics with a proof assistant: no more LSD trip proofs. Zbl 1325.68005 Nipkow, Tobias 4 2012 Proving concurrent noninterference. Zbl 1383.68014 Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 3 2012 Verifying pCTL model checking. Zbl 1352.68154 Hölzl, Johannes; Nipkow, Tobias 2 2012 A compiled implementation of normalisation by evaluation. Zbl 1248.68130 Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias 2 2012 Abstract interpretation of annotated commands. Zbl 1360.68762 Nipkow, Tobias 2 2012 Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214 Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias 25 2011 Verified efficient enumeration of plane graphs modulo isomorphism. Zbl 1342.68298 Nipkow, Tobias 4 2011 Proof pearl: the marriage theorem. Zbl 1350.68237 Jiang, Dongchen; Nipkow, Tobias 1 2011 Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326 Blanchette, Jasmin Christian; Nipkow, Tobias 60 2010 Code generation via higher-order rewrite systems. Zbl 1284.68131 Haftmann, Florian; Nipkow, Tobias 50 2010 Sledgehammer: judgement day. Zbl 1291.68327 Böhme, Sascha; Nipkow, Tobias 35 2010 A revision of the proof of the Kepler conjecture. Zbl 1195.52004 Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland 17 2010 Linear quantifier elimination. Zbl 1207.68339 Nipkow, Tobias 8 2010 Flyspeck II: The basic linear programs. Zbl 1184.68465 Obua, Steven; Nipkow, Tobias 14 2009 Social choice theory in HOL. Arrow and Gibbard-Satterthwaite. Zbl 1185.68631 Nipkow, Tobias 10 2009 Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Zbl 1173.68002 3 2009 Nominal verification of algorithm \(W\). Zbl 1195.68118 Urban, Christian; Nipkow, Tobias 2 2009 The Isabelle framework. Zbl 1165.68478 Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias 28 2008 Linear quantifier elimination. Zbl 1165.68465 Nipkow, Tobias 8 2008 A compiled implementation of normalization by evaluation. Zbl 1165.68442 Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias 5 2008 Proof synthesis and reflection for linear arithmetic. Zbl 1171.03006 Chaieb, Amine; Nipkow, Tobias 4 2008 Finding lexicographic orders for termination proofs in Isabelle/HOL. Zbl 1144.68352 Bulwahn, Lukas; Krauss, Alexander; Nipkow, Tobias 10 2007 Flyspeck I: Tame graphs. Zbl 1222.52018 Nipkow, Tobias; Bauer, Gertrud; Schultz, Paula 16 2006 Verifying a hotel key card system. Zbl 1168.68542 Nipkow, Tobias 4 2006 Proving pointer programs in higher-order logic. Zbl 1081.68008 Mehta, Farhad; Nipkow, Tobias 17 2005 Proof pearl: Defining functions over finite sets. Zbl 1152.68529 Nipkow, Tobias; Paulson, Lawrence C. 10 2005 Verifying and reflecting quantifier elimination for Presburger arithmetic. Zbl 1143.03334 Chaieb, Amine; Nipkow, Tobias 5 2005 Asserting bytecode safety. Zbl 1108.68432 Wildmoser, Martin; Nipkow, Tobias 2 2005 Certifying machine code safety: Shallow versus deep embedding. Zbl 1099.68545 Wildmoser, Martin; Nipkow, Tobias 9 2004 Prototyping proof carrying code. Zbl 1094.68015 Wildmoser, Martin; Nipkow, Tobias; Klein, Gerwin; Nanz, Sebastian 2 2004 Verified bytecode verifiers. Zbl 1038.68109 Klein, Gerwin; Nipkow, Tobias 16 2003 Structured proofs in Isar/HOL. Zbl 1023.68657 Nipkow, Tobias 8 2003 Proving pointer programs in higher-order logic. Zbl 1278.68274 Mehta, Farhad; Nipkow, Tobias 6 2003 Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131 Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus 488 2002 Hoare logics in Isabelle/HOL. Zbl 1097.68632 Nipkow, Tobias 25 2002 Executing higher order logic. Zbl 1054.68133 Berghofer, Stefan; Nipkow, Tobias 22 2002 Hoare logics for recursive procedures and unbounded nondeterminism. Zbl 1020.03029 Nipkow, Tobias 14 2002 Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. Zbl 1064.68543 von Oheimb, David; Nipkow, Tobias 10 2002 The 5 colour theorem in Isabelle/Isar. Zbl 1013.68200 Bauer, Gertrud; Nipkow, Tobias 3 2002 More Church-Rosser proofs (in Isabelle/HOL). Zbl 0958.03011 Nipkow, Tobias 15 2001 Verified lightweight bytecode verification. Zbl 0997.68018 Klein, Gerwin; Nipkow, Tobias 6 2001 Verified bytecode verifiers. Zbl 0978.68512 Nipkow, Tobias 5 2001 Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Zbl 0968.00052 4 2001 Proof terms for simply typed higher order logic. Zbl 0974.03013 Berghofer, Stefan; Nipkow, Tobias 10 2000 \(\mu\)Java: Embedding a programming language in a theorem prover. Zbl 0995.68019 Nipkow, Tobias; von Oheimb, David; Pusch, Cornelia 5 2000 Term rewriting and all that. Zbl 0948.68098 Baader, Franz; Nipkow, Tobias 350 1999 HOLCF=HOL+LCF. Zbl 0933.03028 Müller, Olaf; Nipkow, Tobias; von Oheimb, David; Slotosch, Oscar 12 1999 Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L. Zbl 0943.68150 Naraschewski, Wolfgang; Nipkow, Tobias 4 1999 Higher-order rewrite systems and their confluence. Zbl 0895.68078 Mayr, Richard; Nipkow, Tobias 38 1998 Winskel is (almost) right: Towards a mechanized semantics textbook. Zbl 0910.68138 Nipkow, Tobias 20 1998 Higher-order rewriting and equational reasoning. Zbl 0970.68081 Nipkow, Tobias; Prehofer, Christian 4 1998 More Church-Rosser proofs (in Isabelle/HOL). Zbl 1412.68248 Nipkow, Tobias 1 1996 Type reconstruction for type classes. Zbl 0833.68025 Nipkow, Tobias; Prehofer, Christian 8 1995 Higher-order algebra, logic, and term rewriting. 1st international workshop, HOA ’93, Amsterdam, the Netherlands, September 23–24, 1993. Selected papers. Zbl 0825.00070 2 1994 TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Zbl 0825.00120 1 1994 Interpreter verification for a functional language. Zbl 1044.68666 Broy, Manfred; Hinkel, Ursula; Nipkow, Tobias; Prehofer, Christian; Schieder, Birgit 1 1994 Orthogonal higher-order rewrite systems are confluent. Zbl 0789.68081 Nipkow, Tobias 13 1993 Reduction and unification in lambda calculi with subtypes. Zbl 0925.03094 Nipkow, Tobias; Qian, Zhenyu 3 1992 Combining matching algorithms: The regular case. Zbl 0767.68069 Nipkow, Tobias 10 1991 Higher-order unification, polymorphism, and subsorts (extended abstract). Zbl 1507.68075 Nipkow, Tobias 7 1991 Modular higher-order \(E\)-unification. Zbl 1503.68144 Nipkow, Tobias; Qian, Zhenyu 4 1991 Ordered rewriting and confluence. Zbl 1509.68120 Martin, Ursula; Nipkow, Tobias 12 1990 Unification in primal algebras, their powers and their varieties. Zbl 0711.68092 Nipkow, Tobias 9 1990 Boolean unification - the story so far. Zbl 0682.68093 Martin, Ursula; Nipkow, Tobias 19 1989 Equational reasoning in Isabelle. Zbl 0683.68081 Nipkow, Tobias 7 1989 Term rewriting and beyond – theorem proving in Isabelle. Zbl 0694.68059 Nipkow, Tobias 5 1989 Combining matching algorithms: the regular case. Zbl 1503.68315 Nipkow, Tobias 4 1989 Unification in Boolean rings. Zbl 0659.68111 Martin, Ursula; Nipkow, Tobias 6 1988 Observing nondeterministic data types. Zbl 0665.68013 Nipkow, Tobias 4 1988 Unification in primal algebras. Zbl 0645.68045 Nipkow, Tobias 2 1988 Are homomorphisms sufficient for behavioural implementations of deterministic and nondeterministic data types? Zbl 0616.68019 Nipkow, Tobias 6 1987 Non-deterministic data types: Models and implementations. Zbl 0564.68013 Nipkow, Tobias 9 1986 Unification in Boolean rings. Zbl 0643.68140 Martin, Ursula; Nipkow, Tobias 5 1986 ...and 1 more Documents all cited Publications top 5 cited Publications all top 5 Cited by 1,716 Authors 40 Nipkow, Tobias 35 Blanchette, Jasmin Christian 29 Paulson, Lawrence Charles 24 Benzmüller, Christoph Ewald 21 Thiemann, René 18 Kaliszyk, Cezary 18 Middeldorp, Aart 16 Popescu, Andrei 15 Giesl, Jürgen 15 Tinelli, Cesare 14 Guttmann, Walter 14 Lochbihler, Andreas 14 Reynolds, Andrew 14 Struth, Georg 13 Urban, Josef 12 Ayala-Rincón, Mauricio 11 Foster, Simon 11 Nishida, Naoki 11 Sternagel, Christian 11 Traytel, Dmitry 11 Waldmann, Uwe 10 Ghilardi, Silvio 10 van Oostrom, Vincent 10 Woodcock, James C. P. 10 Yamada, Akihisa 9 Baader, Franz 9 Barrett, Clark W. 9 Kapur, Deepak 9 Lammich, Peter 9 Moser, Georg 9 Schneider-Kamp, Peter 9 Zankl, Harald 8 Avigad, Jeremy 8 Bentkamp, Alexander 8 Fernández, Maribel 8 Klein, Gerwin 8 Marić, Filip 8 Rabe, Florian 8 Ringeissen, Christophe 8 Sutcliffe, Geoff 8 Tourret, Sophie 8 Urban, Christian 8 Vidal, Germán 8 Wenzel, Makarius 8 Wolff, Burkhart 7 Aransay, Jesús 7 Beringer, Lennart 7 Böhme, Sascha 7 Divasón, Jose 7 Felgenhauer, Bertram 7 Fuhs, Carsten 7 Hirokawa, Nao 7 Kohlhase, Michael 7 Krauss, Alexander 7 Kuncak, Viktor 7 Moreira, Nelma 7 Narendran, Paliath 7 Preoteasa, Viorel 7 Vukmirović, Petar 7 Weidenbach, Christoph 6 Brown, Chad Edward 6 Fleury, Mathias 6 Gabbay, Murdoch James 6 Gao, Xing 6 Gauthier, Thibault 6 Godoy, Guillem 6 Guo, Li 6 Johansson, Moa 6 Kirchner, Claude 6 Kumar, Ramana 6 Kunčar, Ondřej 6 Lucas, Salvador 6 Pichardie, David 6 Platzer, André 6 Qian, Zhenyu 6 Schmidt-Schauß, Manfred 6 Steen, Alexander 6 Weber, Tjark 6 Winkler, Sarah 5 Abdulaziz, Mohammad 5 Albert, Elvira 5 Aoto, Takahito 5 Basin, David A. 5 Blanqui, Frédéric 5 Broda, Sabine 5 Brucker, Achim D. 5 Cain, Alan J. 5 Cavalcanti, Ana 5 Echenim, Mnacho 5 Fontaine, Pascal 5 Fuenmayor, David 5 Haftmann, Florian 5 Hofmann, Martin 5 Hölzl, Johannes 5 Immler, Fabian 5 Jouannaud, Jean-Pierre 5 Kirchner, Hélène 5 Malbos, Philippe 5 Marshall, Andrew M. 5 Martí-Oliet, Narciso ...and 1,616 more Authors all top 5 Cited in 126 Serials 206 Journal of Automated Reasoning 57 Theoretical Computer Science 35 Formal Aspects of Computing 27 Information and Computation 27 Logical Methods in Computer Science 27 Journal of Logical and Algebraic Methods in Programming 23 Journal of Symbolic Computation 23 MSCS. Mathematical Structures in Computer Science 19 Formal Methods in System Design 19 Journal of Functional Programming 15 Annals of Mathematics and Artificial Intelligence 12 ACM Transactions on Computational Logic 11 Acta Informatica 10 Applicable Algebra in Engineering, Communication and Computing 10 Theory and Practice of Logic Programming 9 The Journal of Logic and Algebraic Programming 9 Mathematics in Computer Science 8 Annals of Pure and Applied Logic 8 International Journal of Algebra and Computation 7 Science of Computer Programming 6 Journal of Applied Logic 5 Information Processing Letters 5 Journal of Applied Non-Classical Logics 4 Artificial Intelligence 4 AI Communications 4 International Journal of Foundations of Computer Science 4 Higher-Order and Symbolic Computation 4 Logica Universalis 4 The Review of Symbolic Logic 3 Algebra Universalis 3 Journal of Algebra 3 Programming and Computer Software 3 Semigroup Forum 3 Studia Logica 3 Synthese 3 Bulletin of the American Mathematical Society. New Series 3 Experimental Mathematics 3 Fundamenta Informaticae 3 Sādhanā 3 Journal of Formalized Reasoning 2 Communications in Mathematical Physics 2 Information Sciences 2 Journal of Pure and Applied Algebra 2 New Generation Computing 2 Discrete & Computational Geometry 2 International Journal of Approximate Reasoning 2 International Journal of Computer Mathematics 2 Distributed Computing 2 Journal of Logic, Language and Information 2 Theory and Applications of Categories 2 RAIRO. Theoretical Informatics and Applications 2 Journal of High Energy Physics 2 Concurrency and Computation: Practice & Experience 2 Computer Languages, Systems & Structures 2 Journal of Algebra and its Applications 2 Algebraic Combinatorics 1 Communications in Algebra 1 Computer Methods in Applied Mechanics and Engineering 1 Discrete Mathematics 1 International Journal of General Systems 1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) 1 Mathematics of Computation 1 The Mathematical Intelligencer 1 ACM Transactions on Mathematical Software 1 Advances in Mathematics 1 Applied Mathematics and Optimization 1 Fuzzy Sets and Systems 1 Geometriae Dedicata 1 Journal of Combinatorial Theory. Series A 1 Journal of Computer and System Sciences 1 Journal of Economic Theory 1 Journal of Mathematical Economics 1 Journal of Philosophical Logic 1 Journal für die Reine und Angewandte Mathematik 1 The Journal of Symbolic Logic 1 Mathematische Zeitschrift 1 Pacific Journal of Mathematics 1 Proceedings of the Japan Academy. Series A 1 SIAM Journal on Computing 1 Bulletin of the Section of Logic 1 Advances in Applied Mathematics 1 Advances in Mathematics (Beijing) 1 Computer Aided Geometric Design 1 Social Choice and Welfare 1 Computational Mechanics 1 Journal of the American Mathematical Society 1 SIAM Journal on Discrete Mathematics 1 Journal of Cryptology 1 Computational Mathematics and Modeling 1 Annals of Operations Research 1 Computational Geometry 1 Journal of Elasticity 1 Pattern Recognition 1 Indagationes Mathematicae. New Series 1 Cybernetics and Systems Analysis 1 Journal of Mathematical Sciences (New York) 1 Advances in Applied Clifford Algebras 1 Journal of Lie Theory 1 The Bulletin of Symbolic Logic 1 Sbornik: Mathematics ...and 26 more Serials all top 5 Cited in 45 Fields 1,171 Computer science (68-XX) 420 Mathematical logic and foundations (03-XX) 34 Combinatorics (05-XX) 28 Information and communication theory, circuits (94-XX) 27 Category theory; homological algebra (18-XX) 24 General algebraic systems (08-XX) 24 Group theory and generalizations (20-XX) 17 Order, lattices, ordered algebraic structures (06-XX) 15 Commutative algebra (13-XX) 15 Convex and discrete geometry (52-XX) 15 Numerical analysis (65-XX) 15 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 14 Associative rings and algebras (16-XX) 12 Operations research, mathematical programming (90-XX) 11 Number theory (11-XX) 10 General and overarching topics; collections (00-XX) 8 Linear and multilinear algebra; matrix theory (15-XX) 7 History and biography (01-XX) 7 Field theory and polynomials (12-XX) 7 Nonassociative rings and algebras (17-XX) 6 Ordinary differential equations (34-XX) 6 Biology and other natural sciences (92-XX) 6 Systems theory; control (93-XX) 5 Quantum theory (81-XX) 5 Mathematics education (97-XX) 4 Real functions (26-XX) 4 Dynamical systems and ergodic theory (37-XX) 4 Geometry (51-XX) 4 Algebraic topology (55-XX) 4 Probability theory and stochastic processes (60-XX) 3 Algebraic geometry (14-XX) 3 Mechanics of particles and systems (70-XX) 2 Several complex variables and analytic spaces (32-XX) 2 Operator theory (47-XX) 2 Calculus of variations and optimal control; optimization (49-XX) 2 Manifolds and cell complexes (57-XX) 2 Mechanics of deformable solids (74-XX) 2 Statistical mechanics, structure of matter (82-XX) 2 Relativity and gravitational theory (83-XX) 1 Partial differential equations (35-XX) 1 Harmonic analysis on Euclidean spaces (42-XX) 1 Functional analysis (46-XX) 1 General topology (54-XX) 1 Fluid mechanics (76-XX) 1 Geophysics (86-XX) Citations by Year Wikidata Timeline The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.