×
Author ID: nipkow.tobias Recent zbMATH articles by "Nipkow, Tobias"
Published as: Nipkow, Tobias
External Links: MGP · Wikidata · dblp · GND · IdRef
Documents Indexed: 112 Publications since 1982, including 3 Books
8 Contributions as Editor
Biographic References: 2 Publications
Co-Authors: 87 Co-Authors with 89 Joint Publications
1,339 Co-Co-Authors
all top 5

Co-Authors

31 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 Kreuzer, Katharina
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 Nazareth, Dieter
1 Nguyen, Quang Truong
1 Nguyen, Tat Thang
1 Pleso, Joseph
1 Pusch, Cornelia
1 Rau, Martin
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 Weikum, Gerhard
1 Wenzel, Markus
1 Wimmer, Simon

Publications by Year

Citations contained in zbMATH Open

103 Publications have been cited 1,961 times in 1,380 Documents Cited by Year
Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131
Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus
523
2002
Term rewriting and all that. Zbl 0948.68098
Baader, Franz; Nipkow, Tobias
363
1999
Concrete semantics. With Isabelle/HOL. Zbl 1410.68004
Nipkow, Tobias; Klein, Gerwin
67
2014
Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326
Blanchette, Jasmin Christian; Nipkow, Tobias
61
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
56
2017
Code generation via higher-order rewrite systems. Zbl 1284.68131
Haftmann, Florian; Nipkow, Tobias
51
2010
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
29
2008
Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214
Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias
27
2011
Hoare logics in Isabelle/HOL. Zbl 1097.68632
Nipkow, Tobias
27
2002
Data refinement in Isabelle/HOL. Zbl 1317.68212
Haftmann, Florian; Krauss, Alexander; Kunčar, Ondřej; Nipkow, Tobias
26
2013
Executing higher order logic. Zbl 1054.68133
Berghofer, Stefan; Nipkow, Tobias
24
2002
Winskel is (almost) right: Towards a mechanized semantics textbook. Zbl 0910.68138
Nipkow, Tobias
21
1998
Proof Pearl: regular expression equivalence and relation algebra. Zbl 1269.68090
Krauss, Alexander; Nipkow, Tobias
21
2012
Boolean unification - the story so far. Zbl 0682.68093
Martin, Ursula; Nipkow, Tobias
20
1989
Proving pointer programs in higher-order logic. Zbl 1081.68008
Mehta, Farhad; Nipkow, Tobias
19
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
19
2010
Flyspeck I: Tame graphs. Zbl 1222.52018
Nipkow, Tobias; Bauer, Gertrud; Schultz, Paula
17
2006
Verified bytecode verifiers. Zbl 1038.68109
Klein, Gerwin; Nipkow, Tobias
17
2003
Hoare logics for recursive procedures and unbounded nondeterminism. Zbl 1020.03029
Nipkow, Tobias
17
2002
More Church-Rosser proofs (in Isabelle/HOL). Zbl 0958.03011
Nipkow, Tobias
16
2001
Ordered rewriting and confluence. Zbl 1509.68120
Martin, Ursula; Nipkow, Tobias
15
1990
Orthogonal higher-order rewrite systems are confluent. Zbl 0789.68081
Nipkow, Tobias
14
1993
Flyspeck II: The basic linear programs. Zbl 1184.68465
Obua, Steven; Nipkow, Tobias
14
2009
Certifying machine code safety: Shallow versus deep embedding. Zbl 1099.68545
Wildmoser, Martin; Nipkow, Tobias
13
2004
HOLCF=HOL+LCF. Zbl 0933.03028
Müller, Olaf; Nipkow, Tobias; von Oheimb, David; Slotosch, Oscar
13
1999
Unified decision procedures for regular expression equivalence. Zbl 1416.68175
Nipkow, Tobias; Traytel, Dmitriy
13
2014
A decidability result about sufficient-completeness of axiomatically specified abstract data types. Zbl 0493.68024
Nipkow, Tobias; Weikum, Gerhard
12
1982
Mining the Archive of Formal Proofs. Zbl 1417.68176
Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias
12
2015
A verified compiler from Isabelle/HOL to CakeML. Zbl 1418.68045
Hupel, Lars; Nipkow, Tobias
11
2018
Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. Zbl 1064.68543
von Oheimb, David; Nipkow, Tobias
11
2002
Type reconstruction for type classes. Zbl 0833.68025
Nipkow, Tobias; Prehofer, Christian
10
1995
Combining matching algorithms: The regular case. Zbl 0767.68069
Nipkow, Tobias
10
1991
Unification in primal algebras, their powers and their varieties. Zbl 0711.68092
Nipkow, Tobias
10
1990
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
Proof pearl: Defining functions over finite sets. Zbl 1152.68529
Nipkow, Tobias; Paulson, Lawrence C.
10
2005
Non-deterministic data types: Models and implementations. Zbl 0564.68013
Nipkow, Tobias
10
1986
Proof terms for simply typed higher order logic. Zbl 0974.03013
Berghofer, Stefan; Nipkow, Tobias
10
2000
Linear quantifier elimination. Zbl 1165.68465
Nipkow, Tobias
9
2008
Proving pointer programs in higher-order logic. Zbl 1278.68274
Mehta, Farhad; Nipkow, Tobias
9
2003
From LCF to Isabelle/HOL. Zbl 1427.68349
Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius
9
2019
Amortized complexity verified. Zbl 1465.68059
Nipkow, Tobias
9
2015
Structured proofs in Isar/HOL. Zbl 1023.68657
Nipkow, Tobias
8
2003
Linear quantifier elimination. Zbl 1207.68339
Nipkow, Tobias
8
2010
Higher-order unification, polymorphism, and subsorts (extended abstract). Zbl 1507.68075
Nipkow, Tobias
8
1991
Automatic functional correctness proofs for functional search trees. Zbl 1478.68065
Nipkow, Tobias
8
2016
Unification in Boolean rings. Zbl 0643.68140
Martin, Ursula; Nipkow, Tobias
8
1986
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
Term rewriting and beyond – theorem proving in Isabelle. Zbl 0694.68059
Nipkow, Tobias
6
1989
Are homomorphisms sufficient for behavioural implementations of deterministic and nondeterministic data types? Zbl 0616.68019
Nipkow, Tobias
6
1987
Verifying and reflecting quantifier elimination for Presburger arithmetic. Zbl 1143.03334
Chaieb, Amine; Nipkow, Tobias
6
2005
Verified lightweight bytecode verification. Zbl 0997.68018
Klein, Gerwin; Nipkow, Tobias
6
2001
Unification in Boolean rings. Zbl 0659.68111
Martin, Ursula; Nipkow, Tobias
6
1988
Formalized proof systems for propositional logic. Zbl 1528.03097
Michaelis, Julius; Nipkow, Tobias
6
2018
A compiled implementation of normalization by evaluation. Zbl 1165.68442
Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias
5
2008
Verified bytecode verifiers. Zbl 0978.68512
Nipkow, Tobias
5
2001
\(\mu\)Java: Embedding a programming language in a theorem prover. Zbl 0995.68019
Nipkow, Tobias; von Oheimb, David; Pusch, Cornelia
5
2000
Modular higher-order \(E\)-unification. Zbl 1503.68144
Nipkow, Tobias; Qian, Zhenyu
5
1991
Verified analysis of random binary tree structures. Zbl 1468.68288
Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias
4
2018
Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Zbl 1173.68002
4
2009
Verifying a hotel key card system. Zbl 1168.68542
Nipkow, Tobias
4
2006
Proof synthesis and reflection for linear arithmetic. Zbl 1171.03006
Chaieb, Amine; Nipkow, Tobias
4
2008
Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L. Zbl 0943.68150
Naraschewski, Wolfgang; Nipkow, Tobias
4
1999
Verified efficient enumeration of plane graphs modulo isomorphism. Zbl 1342.68298
Nipkow, Tobias
4
2011
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
Teaching semantics with a proof assistant: no more LSD trip proofs. Zbl 1325.68005
Nipkow, Tobias
4
2012
Combining matching algorithms: the regular case. Zbl 1503.68315
Nipkow, Tobias
4
1989
Verified root-balanced trees. Zbl 1503.68052
Nipkow, Tobias
4
2017
Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1323.68346
Traytel, Dmitriy; Nipkow, Tobias
4
2013
Observing nondeterministic data types. Zbl 0665.68013
Nipkow, Tobias
4
1988
Hoare logics for time bounds. A study in meta theory. Zbl 1423.68098
Haslbeck, Maximilian P. L.; Nipkow, Tobias
3
2018
Isabelle’s metalogic: formalization and proof checker. Zbl 07437074
Nipkow, Tobias; Roßkopf, Simon
3
2021
Reduction and unification in lambda calculi with subtypes. Zbl 0925.03094
Nipkow, Tobias; Qian, Zhenyu
3
1992
Rewriting techniques and applications. 9th international conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998. Proceedings. Zbl 0888.00017
3
1998
The 5 colour theorem in Isabelle/Isar. Zbl 1013.68200
Bauer, Gertrud; Nipkow, Tobias
3
2002
Proving concurrent noninterference. Zbl 1383.68014
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
3
2012
Amortized complexity verified. Zbl 1465.68060
Nipkow, Tobias; Brinkop, Hauke
3
2019
Formalizing probabilistic noninterference. Zbl 1426.68287
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
3
2013
Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. Zbl 07649972
Lammich, Peter; Nipkow, Tobias
3
2019
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
3
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
Abstract interpretation of annotated commands. Zbl 1360.68762
Nipkow, Tobias
2
2012
A compiled implementation of normalisation by evaluation. Zbl 1248.68130
Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias
2
2012
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
Verified memoization and dynamic programming. Zbl 1511.68094
Wimmer, Simon; Hu, Shuwei; Nipkow, Tobias
2
2018
Nominal verification of algorithm \(W\). Zbl 1195.68118
Urban, Christian; Nipkow, Tobias
2
2009
Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference. Zbl 1394.68083
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
2
2013
Verified textbook algorithms. A biased survey. Zbl 1517.68443
Nipkow, Tobias; Eberl, Manuel; Haslbeck, Maximilian P. L.
2
2020
Verifying pCTL model checking. Zbl 1352.68154
Hölzl, Johannes; Nipkow, Tobias
2
2012
TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Zbl 0825.00120
1
1994
Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1420.68049
Traytel, Dmitriy; Nipkow, Tobias
1
2015
Proof pearl: the marriage theorem. Zbl 1350.68237
Jiang, Dongchen; Nipkow, Tobias
1
2011
Interpreter verification for a functional language. Zbl 1044.68666
Broy, Manfred; Hinkel, Ursula; Nipkow, Tobias; Prehofer, Christian; Schieder, Birgit
1
1994
Verified approximation algorithms. Zbl 07614677
Eßmann, Robin; Nipkow, Tobias; Robillard, Simon
1
2020
Isabelle’s metalogic: formalization and proof checker. Zbl 07437074
Nipkow, Tobias; Roßkopf, Simon
3
2021
A verified decision procedure for orders in Isabelle/HOL. Zbl 1497.68549
Stevens, Lukas; Nipkow, Tobias
1
2021
Verified analysis of random binary tree structures. Zbl 1468.68289
Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias
3
2020
Verified textbook algorithms. A biased survey. Zbl 1517.68443
Nipkow, Tobias; Eberl, Manuel; Haslbeck, Maximilian P. L.
2
2020
Verified approximation algorithms. Zbl 07614677
Eßmann, Robin; Nipkow, Tobias; Robillard, Simon
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
11
2018
Formalized proof systems for propositional logic. Zbl 1528.03097
Michaelis, Julius; Nipkow, Tobias
6
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
56
2017
Verified root-balanced trees. Zbl 1503.68052
Nipkow, Tobias
4
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
12
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
67
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
21
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
Abstract interpretation of annotated commands. Zbl 1360.68762
Nipkow, Tobias
2
2012
A compiled implementation of normalisation by evaluation. Zbl 1248.68130
Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias
2
2012
Verifying pCTL model checking. Zbl 1352.68154
Hölzl, Johannes; Nipkow, Tobias
2
2012
Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214
Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias
27
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
61
2010
Code generation via higher-order rewrite systems. Zbl 1284.68131
Haftmann, Florian; Nipkow, Tobias
51
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
19
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
4
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
29
2008
Linear quantifier elimination. Zbl 1165.68465
Nipkow, Tobias
9
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
17
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
19
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
6
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
13
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
17
2003
Proving pointer programs in higher-order logic. Zbl 1278.68274
Mehta, Farhad; Nipkow, Tobias
9
2003
Structured proofs in Isar/HOL. Zbl 1023.68657
Nipkow, Tobias
8
2003
Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131
Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus
523
2002
Hoare logics in Isabelle/HOL. Zbl 1097.68632
Nipkow, Tobias
27
2002
Executing higher order logic. Zbl 1054.68133
Berghofer, Stefan; Nipkow, Tobias
24
2002
Hoare logics for recursive procedures and unbounded nondeterminism. Zbl 1020.03029
Nipkow, Tobias
17
2002
Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. Zbl 1064.68543
von Oheimb, David; Nipkow, Tobias
11
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
16
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
363
1999
HOLCF=HOL+LCF. Zbl 0933.03028
Müller, Olaf; Nipkow, Tobias; von Oheimb, David; Slotosch, Oscar
13
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
21
1998
Higher-order rewriting and equational reasoning. Zbl 0970.68081
Nipkow, Tobias; Prehofer, Christian
4
1998
Rewriting techniques and applications. 9th international conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998. Proceedings. Zbl 0888.00017
3
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
10
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
14
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
8
1991
Modular higher-order \(E\)-unification. Zbl 1503.68144
Nipkow, Tobias; Qian, Zhenyu
5
1991
Ordered rewriting and confluence. Zbl 1509.68120
Martin, Ursula; Nipkow, Tobias
15
1990
Unification in primal algebras, their powers and their varieties. Zbl 0711.68092
Nipkow, Tobias
10
1990
Boolean unification - the story so far. Zbl 0682.68093
Martin, Ursula; Nipkow, Tobias
20
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
6
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
3
1988
Are homomorphisms sufficient for behavioural implementations of deterministic and nondeterministic data types? Zbl 0616.68019
Nipkow, Tobias
6
1987
...and 3 more Documents
all top 5

Cited by 1,834 Authors

42 Nipkow, Tobias
37 Blanchette, Jasmin Christian
30 Paulson, Lawrence Charles
24 Benzmüller, Christoph Ewald
21 Thiemann, René
20 Middeldorp, Aart
18 Kaliszyk, Cezary
18 Popescu, Andrei
16 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
12 Traytel, Dmitry
11 Foster, Simon
11 Lammich, Peter
11 Nishida, Naoki
11 Sternagel, Christian
11 Waldmann, Uwe
10 Avigad, Jeremy
10 Ghilardi, Silvio
10 Klein, Gerwin
10 van Oostrom, Vincent
10 Woodcock, James C. P.
10 Yamada, Akihisa
9 Baader, Franz
9 Barrett, Clark W.
9 Fernández, Maribel
9 Hirokawa, Nao
9 Kapur, Deepak
9 Moser, Georg
9 Schneider-Kamp, Peter
9 Sutcliffe, Geoff
9 Tourret, Sophie
9 Zankl, Harald
8 Bentkamp, Alexander
8 Beringer, Lennart
8 Charguéraud, Arthur
8 Krauss, Alexander
8 Kuncak, Viktor
8 Marić, Filip
8 Preoteasa, Viorel
8 Rabe, Florian
8 Ringeissen, Christophe
8 Urban, Christian
8 Vidal, Germán
8 Wenzel, Makarius
8 Wolff, Burkhart
7 Aransay, Jesús
7 Böhme, Sascha
7 Divasón, Jose
7 Felgenhauer, Bertram
7 Fleury, Mathias
7 Fuhs, Carsten
7 Kohlhase, Michael
7 Moreira, Nelma
7 Narendran, Paliath
7 Pous, Damien
7 Schmidt-Schauß, Manfred
7 Vukmirović, Petar
7 Weber, Tjark
7 Weidenbach, Christoph
6 Aoto, Takahito
6 Brown, Chad Edward
6 Gabbay, Murdoch James
6 Gao, Xing
6 Gauthier, Thibault
6 Godoy, Guillem
6 Guo, Li
6 Hölzl, Johannes
6 Johansson, Moa
6 Kirchner, Claude
6 Kumar, Ramana
6 Kunčar, Ondřej
6 Lucas, Salvador
6 Norrish, Michael
6 Pichardie, David
6 Platzer, André
6 Qian, Zhenyu
6 Winkler, Sarah
5 Abdulaziz, Mohammad
5 Albert, Elvira
5 Barthe, Gilles
5 Basin, David A.
5 Birkedal, Lars
5 Blanqui, Frédéric
5 Broda, Sabine
5 Brucker, Achim D.
5 Cain, Alan J.
5 Cavalcanti, Ana
5 Dongol, Brijesh
5 Echenim, Mnacho
5 Fleuriot, Jacques D.
5 Fontaine, Pascal
5 Fuenmayor, David
5 Haftmann, Florian
5 Hofmann, Martin
...and 1,734 more Authors
all top 5

Cited in 131 Serials

209 Journal of Automated Reasoning
59 Theoretical Computer Science
36 Formal Aspects of Computing
29 Logical Methods in Computer Science
29 Journal of Logical and Algebraic Methods in Programming
28 Information and Computation
27 Journal of Symbolic Computation
23 Mathematical Structures in Computer Science
20 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
7 Bulletin of the American Mathematical Society. New Series
6 Information Processing Letters
6 Journal of Applied Logic
5 AI Communications
5 Journal of Applied Non-Classical Logics
4 Artificial Intelligence
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 Experimental Mathematics
3 Fundamenta Informaticae
3 Sādhanā
3 Journal of Formalized Reasoning
2 Communications in Mathematical Physics
2 Information Sciences
2 Journal of Combinatorial Theory. Series A
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 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 Journal of Artificial Intelligence Research (JAIR)
1 The Bulletin of Symbolic Logic
...and 31 more Serials
all top 5

Cited in 46 Fields

1,262 Computer science (68-XX)
429 Mathematical logic and foundations (03-XX)
37 Combinatorics (05-XX)
30 Information and communication theory, circuits (94-XX)
28 Category theory; homological algebra (18-XX)
25 General algebraic systems (08-XX)
25 Group theory and generalizations (20-XX)
17 Order, lattices, ordered algebraic structures (06-XX)
17 Numerical analysis (65-XX)
16 Commutative algebra (13-XX)
16 Convex and discrete geometry (52-XX)
16 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
15 Number theory (11-XX)
15 Associative rings and algebras (16-XX)
14 General and overarching topics; collections (00-XX)
14 Operations research, mathematical programming (90-XX)
10 Linear and multilinear algebra; matrix theory (15-XX)
9 History and biography (01-XX)
7 Field theory and polynomials (12-XX)
7 Nonassociative rings and algebras (17-XX)
7 Systems theory; control (93-XX)
6 Ordinary differential equations (34-XX)
6 Quantum theory (81-XX)
6 Biology and other natural sciences (92-XX)
6 Mathematics education (97-XX)
5 Algebraic geometry (14-XX)
5 Geometry (51-XX)
4 Real functions (26-XX)
4 Dynamical systems and ergodic theory (37-XX)
4 Algebraic topology (55-XX)
4 Probability theory and stochastic processes (60-XX)
3 Operator theory (47-XX)
3 Mechanics of particles and systems (70-XX)
2 Several complex variables and analytic spaces (32-XX)
2 Functional analysis (46-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 Measure and integration (28-XX)
1 Partial differential equations (35-XX)
1 Harmonic analysis on Euclidean spaces (42-XX)
1 General topology (54-XX)
1 Fluid mechanics (76-XX)
1 Geophysics (86-XX)

Citations by Year

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.