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: 107 Publications since 1982, including 3 Books 8 Contributions as Editor Biographic References: 2 Publications Co-Authors: 84 Co-Authors with 85 Joint Publications 1,302 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 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 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 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 112 Computer science (68-XX) 37 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 97 Publications have been cited 1,724 times in 1,207 Documents Cited by ▼ Year ▼ Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus 461 2002 Term rewriting and all that. Zbl 0948.68098Baader, Franz; Nipkow, Tobias 335 1999 Concrete semantics. With Isabelle/HOL. Zbl 1410.68004Nipkow, Tobias; Klein, Gerwin 56 2014 Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326Blanchette, Jasmin Christian; Nipkow, Tobias 54 2010 Code generation via higher-order rewrite systems. Zbl 1284.68131Haftmann, Florian; Nipkow, Tobias 50 2010 A formal proof of the Kepler conjecture. Zbl 1379.52018Hales, 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 35 2017 Higher-order rewrite systems and their confluence. Zbl 0895.68078Mayr, Richard; Nipkow, Tobias 35 1998 Sledgehammer: judgement day. Zbl 1291.68327Böhme, Sascha; Nipkow, Tobias 34 2010 Data refinement in Isabelle/HOL. Zbl 1317.68212Haftmann, Florian; Krauss, Alexander; Kunčar, Ondřej; Nipkow, Tobias 26 2013 The Isabelle framework. Zbl 1165.68478Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias 26 2008 Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias 24 2011 Executing higher order logic. Zbl 1054.68133Berghofer, Stefan; Nipkow, Tobias 22 2002 Hoare logics in Isabelle/HOL. Zbl 1097.68632Nipkow, Tobias 22 2002 Boolean unification - the story so far. Zbl 0682.68093Martin, Ursula; Nipkow, Tobias 19 1989 Proof Pearl: regular expression equivalence and relation algebra. Zbl 1269.68090Krauss, Alexander; Nipkow, Tobias 18 2012 Winskel is (almost) right: Towards a mechanized semantics textbook. Zbl 0910.68138Nipkow, Tobias 18 1998 Proving pointer programs in higher-order logic. Zbl 1081.68008Mehta, Farhad; Nipkow, Tobias 17 2005 Flyspeck I: Tame graphs. Zbl 1222.52018Nipkow, Tobias; Bauer, Gertrud; Schultz, Paula 16 2006 A revision of the proof of the Kepler conjecture. Zbl 1195.52004Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland 16 2010 Verified bytecode verifiers. Zbl 1038.68109Klein, Gerwin; Nipkow, Tobias 16 2003 More Church-Rosser proofs (in Isabelle/HOL). Zbl 0958.03011Nipkow, Tobias 15 2001 Hoare logics for recursive procedures and unbounded nondeterminism. Zbl 1020.03029Nipkow, Tobias 14 2002 Flyspeck II: The basic linear programs. Zbl 1184.68465Obua, Steven; Nipkow, Tobias 13 2009 HOLCF=HOL+LCF. Zbl 0933.03028Müller, Olaf; Nipkow, Tobias; von Oheimb, David; Slotosch, Oscar 12 1999 Unified decision procedures for regular expression equivalence. Zbl 1416.68175Nipkow, Tobias; Traytel, Dmitriy 12 2014 Orthogonal higher-order rewrite systems are confluent. Zbl 0789.68081Nipkow, Tobias 12 1993 Combining matching algorithms: The regular case. Zbl 0767.68069Nipkow, Tobias 10 1991 A decidability result about sufficient-completeness of axiomatically specified abstract data types. Zbl 0493.68024Nipkow, Tobias; Weikum, Gerhard 10 1982 Finding lexicographic orders for termination proofs in Isabelle/HOL. Zbl 1144.68352Bulwahn, Lukas; Krauss, Alexander; Nipkow, Tobias 10 2007 Proof pearl: Defining functions over finite sets. Zbl 1152.68529Nipkow, Tobias; Paulson, Lawrence C. 10 2005 Mining the Archive of Formal Proofs. Zbl 1417.68176Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias 10 2015 Social choice theory in HOL. Arrow and Gibbard-Satterthwaite. Zbl 1185.68631Nipkow, Tobias 10 2009 Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. Zbl 1064.68543von Oheimb, David; Nipkow, Tobias 10 2002 Proof terms for simply typed higher order logic. Zbl 0974.03013Berghofer, Stefan; Nipkow, Tobias 10 2000 Unification in primal algebras, their powers and their varieties. Zbl 0711.68092Nipkow, Tobias 9 1990 Amortized complexity verified. Zbl 1465.68059Nipkow, Tobias 9 2015 A verified compiler from Isabelle/HOL to CakeML. Zbl 1418.68045Hupel, Lars; Nipkow, Tobias 9 2018 Non-deterministic data types: Models and implementations. Zbl 0564.68013Nipkow, Tobias 9 1986 Linear quantifier elimination. Zbl 1165.68465Nipkow, Tobias 8 2008 Automatic functional correctness proofs for functional search trees. Zbl 1478.68065Nipkow, Tobias 8 2016 Type reconstruction for type classes. Zbl 0833.68025Nipkow, Tobias; Prehofer, Christian 8 1995 Structured proofs in Isar/HOL. Zbl 1023.68657Nipkow, Tobias 8 2003 Certifying machine code safety: Shallow versus deep embedding. Zbl 1099.68545Wildmoser, Martin; Nipkow, Tobias 8 2004 A verified compiler for probability density functions. Zbl 1335.68037Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias 7 2015 Higher-order unification, polymorphism, and subsorts (extended abstract). Zbl 1507.68075Nipkow, Tobias 7 1991 Equational reasoning in Isabelle. Zbl 0683.68081Nipkow, Tobias 6 1989 Unification in Boolean rings. Zbl 0659.68111Martin, Ursula; Nipkow, Tobias 6 1988 Linear quantifier elimination. Zbl 1207.68339Nipkow, Tobias 6 2010 Proving pointer programs in higher-order logic. Zbl 1278.68274Mehta, Farhad; Nipkow, Tobias 6 2003 Are homomorphisms sufficient for behavioural implementations of deterministic and nondeterministic data types? Zbl 0616.68019Nipkow, Tobias 6 1987 Verified lightweight bytecode verification. Zbl 0997.68018Klein, Gerwin; Nipkow, Tobias 6 2001 Ordered rewriting and confluence. Zbl 1509.68120Martin, Ursula; Nipkow, Tobias 6 1990 Term rewriting and beyond – theorem proving in Isabelle. Zbl 0694.68059Nipkow, Tobias 5 1989 Verifying and reflecting quantifier elimination for Presburger arithmetic. Zbl 1143.03334Chaieb, Amine; Nipkow, Tobias 5 2005 A compiled implementation of normalization by evaluation. Zbl 1165.68442Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias 5 2008 Unification in Boolean rings. Zbl 0643.68140Martin, Ursula; Nipkow, Tobias 5 1986 From LCF to Isabelle/HOL. Zbl 1427.68349Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius 5 2019 Verified bytecode verifiers. Zbl 0978.68512Nipkow, Tobias 5 2001 \(\mu\)Java: Embedding a programming language in a theorem prover. Zbl 0995.68019Nipkow, Tobias; von Oheimb, David; Pusch, Cornelia 5 2000 Proof synthesis and reflection for linear arithmetic. Zbl 1171.03006Chaieb, Amine; Nipkow, Tobias 4 2008 Verifying a hotel key card system. Zbl 1168.68542Nipkow, Tobias 4 2006 Verified efficient enumeration of plane graphs modulo isomorphism. Zbl 1342.68298Nipkow, Tobias 4 2011 Teaching semantics with a proof assistant: no more LSD trip proofs. Zbl 1325.68005Nipkow, Tobias 4 2012 Modular higher-order \(E\)-unification. Zbl 1503.68144Nipkow, Tobias; Qian, Zhenyu 4 1991 Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L. Zbl 0943.68150Naraschewski, Wolfgang; Nipkow, Tobias 4 1999 Higher-order rewriting and equational reasoning. Zbl 0970.68081Nipkow, 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 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1323.68346Traytel, Dmitriy; Nipkow, Tobias 4 2013 Observing nondeterministic data types. Zbl 0665.68013Nipkow, Tobias 3 1988 Formalizing probabilistic noninterference. Zbl 1426.68287Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 3 2013 Amortized complexity verified. Zbl 1465.68060Nipkow, Tobias; Brinkop, Hauke 3 2019 Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Zbl 1173.68002 3 2009 Verified analysis of random binary tree structures. Zbl 1468.68288Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias 3 2018 Combining matching algorithms: the regular case. Zbl 1503.68315Nipkow, Tobias 3 1989 Hoare logics for time bounds. A study in meta theory. Zbl 1423.68098Haslbeck, Maximilian P. L.; Nipkow, Tobias 3 2018 Reduction and unification in lambda calculi with subtypes. Zbl 0925.03094Nipkow, Tobias; Qian, Zhenyu 3 1992 The 5 colour theorem in Isabelle/Isar. Zbl 1013.68200Bauer, Gertrud; Nipkow, Tobias 3 2002 Proving concurrent noninterference. Zbl 1383.68014Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 3 2012 Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference. Zbl 1394.68083Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 2 2013 Unification in primal algebras. Zbl 0645.68045Nipkow, 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 Nominal verification of algorithm \(W\). Zbl 1195.68118Urban, Christian; Nipkow, Tobias 2 2009 Verifying pCTL model checking. Zbl 1352.68154Hölzl, Johannes; Nipkow, Tobias 2 2012 A compiled implementation of normalisation by evaluation. Zbl 1248.68130Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias 2 2012 Abstract interpretation of annotated commands. Zbl 1360.68762Nipkow, Tobias 2 2012 Verified memoization and dynamic programming. Zbl 1511.68094Wimmer, Simon; Hu, Shuwei; Nipkow, Tobias 2 2018 Verified analysis of random binary tree structures. Zbl 1468.68289Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias 2 2020 Verified root-balanced trees. Zbl 1503.68052Nipkow, Tobias 2 2017 Proof pearl: purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. Zbl 07649972Lammich, Peter; Nipkow, Tobias 2 2019 Prototyping proof carrying code. Zbl 1094.68015Wildmoser, Martin; Nipkow, Tobias; Klein, Gerwin; Nanz, Sebastian 2 2004 Asserting bytecode safety. Zbl 1108.68432Wildmoser, Martin; Nipkow, Tobias 2 2005 Isabelle’s metalogic: formalization and proof checker. Zbl 07437074Nipkow, Tobias; Roßkopf, Simon 2 2021 TYPES ’93, Types for proofs and programs. International Workshop, Nijmegen, the Netherlands, May 24-28, 1993. Selected papers. Zbl 0825.00120 1 1994 More Church-Rosser proofs (in Isabelle/HOL). Zbl 1412.68248Nipkow, Tobias 1 1996 Proof pearl: the marriage theorem. Zbl 1350.68237Jiang, Dongchen; Nipkow, Tobias 1 2011 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1420.68049Traytel, Dmitriy; Nipkow, Tobias 1 2015 Trustworthy graph algorithms (Invited Talk). Zbl 07561645Abdulaziz, Mohammad; Mehlhorn, Kurt; Nipkow, Tobias 1 2019 Isabelle’s metalogic: formalization and proof checker. Zbl 07437074Nipkow, Tobias; Roßkopf, Simon 2 2021 Verified analysis of random binary tree structures. Zbl 1468.68289Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias 2 2020 From LCF to Isabelle/HOL. Zbl 1427.68349Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius 5 2019 Amortized complexity verified. Zbl 1465.68060Nipkow, Tobias; Brinkop, Hauke 3 2019 Proof pearl: purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. Zbl 07649972Lammich, Peter; Nipkow, Tobias 2 2019 Trustworthy graph algorithms (Invited Talk). Zbl 07561645Abdulaziz, Mohammad; Mehlhorn, Kurt; Nipkow, Tobias 1 2019 A verified compiler from Isabelle/HOL to CakeML. Zbl 1418.68045Hupel, Lars; Nipkow, Tobias 9 2018 Verified analysis of random binary tree structures. Zbl 1468.68288Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias 3 2018 Hoare logics for time bounds. A study in meta theory. Zbl 1423.68098Haslbeck, Maximilian P. L.; Nipkow, Tobias 3 2018 Verified memoization and dynamic programming. Zbl 1511.68094Wimmer, Simon; Hu, Shuwei; Nipkow, Tobias 2 2018 A formal proof of the Kepler conjecture. Zbl 1379.52018Hales, 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 35 2017 Verified root-balanced trees. Zbl 1503.68052Nipkow, Tobias 2 2017 Automatic functional correctness proofs for functional search trees. Zbl 1478.68065Nipkow, Tobias 8 2016 Mining the Archive of Formal Proofs. Zbl 1417.68176Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias 10 2015 Amortized complexity verified. Zbl 1465.68059Nipkow, Tobias 9 2015 A verified compiler for probability density functions. Zbl 1335.68037Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias 7 2015 Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1420.68049Traytel, Dmitriy; Nipkow, Tobias 1 2015 Concrete semantics. With Isabelle/HOL. Zbl 1410.68004Nipkow, Tobias; Klein, Gerwin 56 2014 Unified decision procedures for regular expression equivalence. Zbl 1416.68175Nipkow, Tobias; Traytel, Dmitriy 12 2014 Data refinement in Isabelle/HOL. Zbl 1317.68212Haftmann, 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.68346Traytel, Dmitriy; Nipkow, Tobias 4 2013 Formalizing probabilistic noninterference. Zbl 1426.68287Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 3 2013 Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference. Zbl 1394.68083Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 2 2013 Proof Pearl: regular expression equivalence and relation algebra. Zbl 1269.68090Krauss, Alexander; Nipkow, Tobias 18 2012 Teaching semantics with a proof assistant: no more LSD trip proofs. Zbl 1325.68005Nipkow, Tobias 4 2012 Proving concurrent noninterference. Zbl 1383.68014Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias 3 2012 Verifying pCTL model checking. Zbl 1352.68154Hölzl, Johannes; Nipkow, Tobias 2 2012 A compiled implementation of normalisation by evaluation. Zbl 1248.68130Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias 2 2012 Abstract interpretation of annotated commands. Zbl 1360.68762Nipkow, Tobias 2 2012 Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias 24 2011 Verified efficient enumeration of plane graphs modulo isomorphism. Zbl 1342.68298Nipkow, Tobias 4 2011 Proof pearl: the marriage theorem. Zbl 1350.68237Jiang, Dongchen; Nipkow, Tobias 1 2011 Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326Blanchette, Jasmin Christian; Nipkow, Tobias 54 2010 Code generation via higher-order rewrite systems. Zbl 1284.68131Haftmann, Florian; Nipkow, Tobias 50 2010 Sledgehammer: judgement day. Zbl 1291.68327Böhme, Sascha; Nipkow, Tobias 34 2010 A revision of the proof of the Kepler conjecture. Zbl 1195.52004Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland 16 2010 Linear quantifier elimination. Zbl 1207.68339Nipkow, Tobias 6 2010 Flyspeck II: The basic linear programs. Zbl 1184.68465Obua, Steven; Nipkow, Tobias 13 2009 Social choice theory in HOL. Arrow and Gibbard-Satterthwaite. Zbl 1185.68631Nipkow, 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.68118Urban, Christian; Nipkow, Tobias 2 2009 The Isabelle framework. Zbl 1165.68478Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias 26 2008 Linear quantifier elimination. Zbl 1165.68465Nipkow, Tobias 8 2008 A compiled implementation of normalization by evaluation. Zbl 1165.68442Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias 5 2008 Proof synthesis and reflection for linear arithmetic. Zbl 1171.03006Chaieb, Amine; Nipkow, Tobias 4 2008 Finding lexicographic orders for termination proofs in Isabelle/HOL. Zbl 1144.68352Bulwahn, Lukas; Krauss, Alexander; Nipkow, Tobias 10 2007 Flyspeck I: Tame graphs. Zbl 1222.52018Nipkow, Tobias; Bauer, Gertrud; Schultz, Paula 16 2006 Verifying a hotel key card system. Zbl 1168.68542Nipkow, Tobias 4 2006 Proving pointer programs in higher-order logic. Zbl 1081.68008Mehta, Farhad; Nipkow, Tobias 17 2005 Proof pearl: Defining functions over finite sets. Zbl 1152.68529Nipkow, Tobias; Paulson, Lawrence C. 10 2005 Verifying and reflecting quantifier elimination for Presburger arithmetic. Zbl 1143.03334Chaieb, Amine; Nipkow, Tobias 5 2005 Asserting bytecode safety. Zbl 1108.68432Wildmoser, Martin; Nipkow, Tobias 2 2005 Certifying machine code safety: Shallow versus deep embedding. Zbl 1099.68545Wildmoser, Martin; Nipkow, Tobias 8 2004 Prototyping proof carrying code. Zbl 1094.68015Wildmoser, Martin; Nipkow, Tobias; Klein, Gerwin; Nanz, Sebastian 2 2004 Verified bytecode verifiers. Zbl 1038.68109Klein, Gerwin; Nipkow, Tobias 16 2003 Structured proofs in Isar/HOL. Zbl 1023.68657Nipkow, Tobias 8 2003 Proving pointer programs in higher-order logic. Zbl 1278.68274Mehta, Farhad; Nipkow, Tobias 6 2003 Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus 461 2002 Executing higher order logic. Zbl 1054.68133Berghofer, Stefan; Nipkow, Tobias 22 2002 Hoare logics in Isabelle/HOL. Zbl 1097.68632Nipkow, Tobias 22 2002 Hoare logics for recursive procedures and unbounded nondeterminism. Zbl 1020.03029Nipkow, Tobias 14 2002 Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. Zbl 1064.68543von Oheimb, David; Nipkow, Tobias 10 2002 The 5 colour theorem in Isabelle/Isar. Zbl 1013.68200Bauer, Gertrud; Nipkow, Tobias 3 2002 More Church-Rosser proofs (in Isabelle/HOL). Zbl 0958.03011Nipkow, Tobias 15 2001 Verified lightweight bytecode verification. Zbl 0997.68018Klein, Gerwin; Nipkow, Tobias 6 2001 Verified bytecode verifiers. Zbl 0978.68512Nipkow, 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.03013Berghofer, Stefan; Nipkow, Tobias 10 2000 \(\mu\)Java: Embedding a programming language in a theorem prover. Zbl 0995.68019Nipkow, Tobias; von Oheimb, David; Pusch, Cornelia 5 2000 Term rewriting and all that. Zbl 0948.68098Baader, Franz; Nipkow, Tobias 335 1999 HOLCF=HOL+LCF. Zbl 0933.03028Müller, Olaf; Nipkow, Tobias; von Oheimb, David; Slotosch, Oscar 12 1999 Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L. Zbl 0943.68150Naraschewski, Wolfgang; Nipkow, Tobias 4 1999 Higher-order rewrite systems and their confluence. Zbl 0895.68078Mayr, Richard; Nipkow, Tobias 35 1998 Winskel is (almost) right: Towards a mechanized semantics textbook. Zbl 0910.68138Nipkow, Tobias 18 1998 Higher-order rewriting and equational reasoning. Zbl 0970.68081Nipkow, Tobias; Prehofer, Christian 4 1998 More Church-Rosser proofs (in Isabelle/HOL). Zbl 1412.68248Nipkow, Tobias 1 1996 Type reconstruction for type classes. Zbl 0833.68025Nipkow, 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 Orthogonal higher-order rewrite systems are confluent. Zbl 0789.68081Nipkow, Tobias 12 1993 Reduction and unification in lambda calculi with subtypes. Zbl 0925.03094Nipkow, Tobias; Qian, Zhenyu 3 1992 Combining matching algorithms: The regular case. Zbl 0767.68069Nipkow, Tobias 10 1991 Higher-order unification, polymorphism, and subsorts (extended abstract). Zbl 1507.68075Nipkow, Tobias 7 1991 Modular higher-order \(E\)-unification. Zbl 1503.68144Nipkow, Tobias; Qian, Zhenyu 4 1991 Unification in primal algebras, their powers and their varieties. Zbl 0711.68092Nipkow, Tobias 9 1990 Ordered rewriting and confluence. Zbl 1509.68120Martin, Ursula; Nipkow, Tobias 6 1990 Boolean unification - the story so far. Zbl 0682.68093Martin, Ursula; Nipkow, Tobias 19 1989 Equational reasoning in Isabelle. Zbl 0683.68081Nipkow, Tobias 6 1989 Term rewriting and beyond – theorem proving in Isabelle. Zbl 0694.68059Nipkow, Tobias 5 1989 Combining matching algorithms: the regular case. Zbl 1503.68315Nipkow, Tobias 3 1989 Unification in Boolean rings. Zbl 0659.68111Martin, Ursula; Nipkow, Tobias 6 1988 Observing nondeterministic data types. Zbl 0665.68013Nipkow, Tobias 3 1988 Unification in primal algebras. Zbl 0645.68045Nipkow, Tobias 2 1988 Are homomorphisms sufficient for behavioural implementations of deterministic and nondeterministic data types? Zbl 0616.68019Nipkow, Tobias 6 1987 Non-deterministic data types: Models and implementations. Zbl 0564.68013Nipkow, Tobias 9 1986 Unification in Boolean rings. Zbl 0643.68140Martin, Ursula; Nipkow, Tobias 5 1986 A decidability result about sufficient-completeness of axiomatically specified abstract data types. Zbl 0493.68024Nipkow, Tobias; Weikum, Gerhard 10 1982 all cited Publications top 5 cited Publications all top 5 Cited by 1,618 Authors 39 Nipkow, Tobias 33 Blanchette, Jasmin Christian 27 Paulson, Lawrence Charles 23 Benzmüller, Christoph Ewald 21 Thiemann, René 18 Kaliszyk, Cezary 17 Middeldorp, Aart 16 Popescu, Andrei 15 Giesl, Jürgen 15 Tinelli, Cesare 14 Lochbihler, Andreas 14 Reynolds, Andrew 14 Struth, Georg 12 Ayala-Rincón, Mauricio 12 Guttmann, Walter 12 Urban, Josef 11 Nishida, Naoki 11 Sternagel, Christian 11 Traytel, Dmitry 11 Waldmann, Uwe 10 Ghilardi, Silvio 10 Yamada, Akihisa 9 Baader, Franz 9 Barrett, Clark W. 9 Foster, Simon 9 Kapur, Deepak 9 Lammich, Peter 9 Moser, Georg 9 Schneider-Kamp, Peter 9 van Oostrom, Vincent 9 Zankl, Harald 8 Avigad, Jeremy 8 Fernández, Maribel 8 Klein, Gerwin 8 Marić, Filip 8 Ringeissen, Christophe 8 Urban, Christian 8 Vidal, Germán 8 Wolff, Burkhart 8 Woodcock, James C. P. 7 Bentkamp, Alexander 7 Beringer, Lennart 7 Böhme, Sascha 7 Felgenhauer, Bertram 7 Krauss, Alexander 7 Kuncak, Viktor 7 Preoteasa, Viorel 7 Rabe, Florian 7 Weidenbach, Christoph 7 Wenzel, Makarius 6 Aransay, Jesús 6 Brown, Chad Edward 6 Divasón, Jose 6 Fleury, Mathias 6 Fuhs, Carsten 6 Gabbay, Murdoch James 6 Gao, Xing 6 Godoy, Guillem 6 Guo, Li 6 Hirokawa, Nao 6 Kirchner, Claude 6 Kunčar, Ondřej 6 Lucas, Salvador 6 Moreira, Nelma 6 Narendran, Paliath 6 Pichardie, David 6 Schmidt-Schauß, Manfred 6 Tourret, Sophie 6 Vukmirović, Petar 6 Weber, Tjark 6 Winkler, Sarah 6 Woltzenlogel Paleo, Bruno 5 Abdulaziz, Mohammad 5 Albert, Elvira 5 Aoto, Takahito 5 Basin, David A. 5 Blanqui, Frédéric 5 Cain, Alan J. 5 Fontaine, Pascal 5 Fuenmayor, David 5 Gauthier, Thibault 5 Haftmann, Florian 5 Hölzl, Johannes 5 Immler, Fabian 5 Johansson, Moa 5 Jouannaud, Jean-Pierre 5 Kirchner, Hélène 5 Kohlhase, Michael 5 Kumar, Ramana 5 Malbos, Philippe 5 Martí-Oliet, Narciso 5 Miller, Dale Allen 5 Narboux, Julien 5 Norrish, Michael 5 Pąk, Karol 5 Platzer, André 5 Pous, Damien 5 Qian, Zhenyu 5 Rizkallah, Christine 5 Sutcliffe, Geoff ...and 1,518 more Authors all top 5 Cited in 122 Serials 201 Journal of Automated Reasoning 57 Theoretical Computer Science 35 Formal Aspects of Computing 26 Information and Computation 26 Logical Methods in Computer Science 25 Journal of Logical and Algebraic Methods in Programming 23 Journal of Symbolic Computation 22 MSCS. Mathematical Structures in Computer Science 19 Journal of Functional Programming 18 Formal Methods in System Design 14 Annals of Mathematics and Artificial Intelligence 12 ACM Transactions on Computational Logic 10 Acta Informatica 9 Applicable Algebra in Engineering, Communication and Computing 9 The Journal of Logic and Algebraic Programming 9 Theory and Practice of Logic Programming 9 Mathematics in Computer Science 8 International Journal of Algebra and Computation 7 Science of Computer Programming 6 Annals of Pure and Applied Logic 6 Journal of Applied Logic 5 Information Processing Letters 5 Journal of Applied Non-Classical Logics 4 Artificial Intelligence 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 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 AI Communications 2 International Journal of Foundations of Computer Science 2 International Journal of Computer Mathematics 2 Bulletin of the American Mathematical Society. New Series 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 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 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 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 1 Computer Aided Geometric Design 1 Social Choice and Welfare 1 Computational Mechanics 1 International Journal of Approximate Reasoning 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 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 1 Constraints 1 Séminaire Lotharingien de Combinatoire 1 Theory of Computing Systems 1 Novi Sad Journal of Mathematics ...and 22 more Serials all top 5 Cited in 42 Fields 1,102 Computer science (68-XX) 396 Mathematical logic and foundations (03-XX) 32 Combinatorics (05-XX) 27 Category theory; homological algebra (18-XX) 25 General algebraic systems (08-XX) 24 Information and communication theory, circuits (94-XX) 23 Group theory and generalizations (20-XX) 17 Order, lattices, ordered algebraic structures (06-XX) 16 Commutative algebra (13-XX) 14 Associative rings and algebras (16-XX) 14 Numerical analysis (65-XX) 14 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 12 Convex and discrete geometry (52-XX) 12 Operations research, mathematical programming (90-XX) 11 Number theory (11-XX) 10 General and overarching topics; collections (00-XX) 7 History and biography (01-XX) 7 Field theory and polynomials (12-XX) 6 Linear and multilinear algebra; matrix theory (15-XX) 6 Ordinary differential equations (34-XX) 6 Biology and other natural sciences (92-XX) 6 Systems theory; control (93-XX) 5 Nonassociative rings and algebras (17-XX) 5 Mathematics education (97-XX) 4 Real functions (26-XX) 4 Dynamical systems and ergodic theory (37-XX) 4 Geometry (51-XX) 4 Probability theory and stochastic processes (60-XX) 4 Quantum theory (81-XX) 3 Algebraic geometry (14-XX) 3 Algebraic topology (55-XX) 3 Mechanics of particles and systems (70-XX) 2 Calculus of variations and optimal control; optimization (49-XX) 2 Mechanics of deformable solids (74-XX) 2 Statistical mechanics, structure of matter (82-XX) 2 Relativity and gravitational theory (83-XX) 1 Several complex variables and analytic spaces (32-XX) 1 Operator theory (47-XX) 1 General topology (54-XX) 1 Manifolds and cell complexes (57-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.