×

zbMATH — the first resource for mathematics

Nipkow, Tobias

Compute Distance To:
Author ID: nipkow.tobias Recent zbMATH articles by "Nipkow, Tobias"
Published as: Nipkow, Tobias
External Links: MGP · Wikidata · dblp
Documents Indexed: 100 Publications since 1982, including 11 Books
Biographic References: 1 Publication

Publications by Year

Citations contained in zbMATH Open

85 Publications have been cited 1,407 times in 1,040 Documents Cited by Year
Term rewriting and all that. Zbl 0948.68098
Baader, Franz; Nipkow, Tobias
448
1999
Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131
Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus
318
2002
Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326
Blanchette, Jasmin Christian; Nipkow, Tobias
38
2010
Code generation via higher-order rewrite systems. Zbl 1284.68131
Haftmann, Florian; Nipkow, Tobias
38
2010
Concrete semantics. With Isabelle/HOL. Zbl 1410.68004
Nipkow, Tobias; Klein, Gerwin
29
2014
Higher-order rewrite systems and their confluence. Zbl 0895.68078
Mayr, Richard; Nipkow, Tobias
26
1998
Sledgehammer: judgement day. Zbl 1291.68327
Böhme, Sascha; Nipkow, Tobias
23
2010
Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214
Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias
19
2011
Data refinement in Isabelle/HOL. Zbl 1317.68212
Haftmann, Florian; Krauss, Alexander; Kunčar, Ondřej; Nipkow, Tobias
17
2013
Executing higher order logic. Zbl 1054.68133
Berghofer, Stefan; Nipkow, Tobias
17
2002
Boolean unification - the story so far. Zbl 0682.68093
Martin, Ursula; Nipkow, Tobias
17
1989
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
16
2017
The Isabelle framework. Zbl 1165.68478
Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias
16
2008
Proving pointer programs in higher-order logic. Zbl 1081.68008
Mehta, Farhad; Nipkow, Tobias
15
2005
Verified bytecode verifiers. Zbl 1038.68109
Klein, Gerwin; Nipkow, Tobias
15
2003
Winskel is (almost) right: Towards a mechanized semantics textbook. Zbl 0910.68138
Nipkow, Tobias
15
1998
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
14
2010
Proof Pearl: regular expression equivalence and relation algebra. Zbl 1269.68090
Krauss, Alexander; Nipkow, Tobias
13
2012
More Church-Rosser proofs (in Isabelle/HOL). Zbl 0958.03011
Nipkow, Tobias
12
2001
Orthogonal higher-order rewrite systems are confluent. Zbl 0789.68081
Nipkow, Tobias
12
1993
Flyspeck II: The basic linear programs. Zbl 1184.68465
Obua, Steven; Nipkow, Tobias
11
2009
Flyspeck I: Tame graphs. Zbl 1222.52018
Nipkow, Tobias; Bauer, Gertrud; Schultz, Paula
11
2006
HOLCF=HOL+LCF. Zbl 0933.03028
Müller, Olaf; Nipkow, Tobias; von Oheimb, David; Slotosch, Oscar
11
1999
Finding lexicographic orders for termination proofs in Isabelle/HOL. Zbl 1144.68352
Bulwahn, Lukas; Krauss, Alexander; Nipkow, Tobias
10
2007
Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. Zbl 1064.68543
von Oheimb, David; Nipkow, Tobias
10
2002
Hoare logics for recursive procedures and unbounded nondeterminism. Zbl 1020.03029
Nipkow, Tobias
10
2002
Combining matching algorithms: The regular case. Zbl 0767.68069
Nipkow, Tobias
10
1991
Proof pearl: Defining functions over finite sets. Zbl 1152.68529
Nipkow, Tobias; Paulson, Lawrence C.
9
2005
Unification in primal algebras, their powers and their varieties. Zbl 0711.68092
Nipkow, Tobias
9
1990
A decidability result about sufficient-completeness of axiomatically specified abstract data types. Zbl 0493.68024
Nipkow, Tobias; Weikum, Gerhard
8
1982
Social choice theory in HOL. Arrow and Gibbard-Satterthwaite. Zbl 1185.68631
Nipkow, Tobias
7
2009
Certifying machine code safety: Shallow versus deep embedding. Zbl 1099.68545
Wildmoser, Martin; Nipkow, Tobias
7
2004
Structured proofs in Isar/HOL. Zbl 1023.68657
Nipkow, Tobias
7
2003
Unification in Boolean rings. Zbl 0643.68140
Martin, Ursula; Nipkow, Tobias
7
1986
Hoare logics in Isabelle/HOL. Zbl 1097.68632
Nipkow, Tobias
6
2002
Proof terms for simply typed higher order logic. Zbl 0974.03013
Berghofer, Stefan; Nipkow, Tobias
6
2000
Unification in Boolean rings. Zbl 0659.68111
Martin, Ursula; Nipkow, Tobias
6
1988
Non-deterministic data types: Models and implementations. Zbl 0564.68013
Nipkow, Tobias
6
1986
Amortized complexity verified. Zbl 06481872
Nipkow, Tobias
5
2015
Unified decision procedures for regular expression equivalence. Zbl 1416.68175
Nipkow, Tobias; Traytel, Dmitriy
5
2014
A compiled implementation of normalization by evaluation. Zbl 1165.68442
Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias
5
2008
Linear quantifier elimination. Zbl 1165.68465
Nipkow, Tobias
5
2008
Verified lightweight bytecode verification. Zbl 0997.68018
Klein, Gerwin; Nipkow, Tobias
5
2001
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
Equational reasoning in Isabelle. Zbl 0683.68081
Nipkow, Tobias
5
1989
Are homomorphisms sufficient for behavioural implementations of deterministic and nondeterministic data types? Zbl 0616.68019
Nipkow, Tobias
5
1987
A verified compiler from Isabelle/HOL to CakeML. Zbl 1418.68045
Hupel, Lars; Nipkow, Tobias
4
2018
Automatic functional correctness proofs for functional search trees. Zbl 06644751
Nipkow, Tobias
4
2016
A verified compiler for probability density functions. Zbl 1335.68037
Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias
4
2015
Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1323.68346
Traytel, Dmitriy; Nipkow, Tobias
4
2013
Proof synthesis and reflection for linear arithmetic. Zbl 1171.03006
Chaieb, Amine; Nipkow, Tobias
4
2008
Verifying and reflecting quantifier elimination for Presburger arithmetic. Zbl 1143.03334
Chaieb, Amine; Nipkow, Tobias
4
2005
Proving pointer programs in higher-order logic. Zbl 1278.68274
Mehta, Farhad; Nipkow, Tobias
4
2003
Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Zbl 0968.00052
Goré, Rajeev (ed.); Leitsch, Alexander (ed.); Nipkow, Tobias (ed.)
4
2001
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
Type reconstruction for type classes. Zbl 0833.68025
Nipkow, Tobias; Prehofer, Christian
4
1995
Teaching semantics with a proof assistant: no more LSD trip proofs. Zbl 1325.68005
Nipkow, Tobias
3
2012
The 5 colour theorem in Isabelle/Isar. Zbl 1013.68200
Bauer, Gertrud; Nipkow, Tobias
3
2002
Reduction and unification in lambda calculi with subtypes. Zbl 0925.03094
Nipkow, Tobias; Qian, Zhenyu
3
1992
Term rewriting and beyond – theorem proving in Isabelle. Zbl 0694.68059
Nipkow, Tobias
3
1989
Verified analysis of random binary tree structures. Zbl 06946981
Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias
2
2018
Mining the Archive of Formal Proofs. Zbl 1417.68176
Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias
2
2015
Formalizing probabilistic noninterference. Zbl 1426.68287
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
2
2013
Verified efficient enumeration of plane graphs modulo isomorphism. Zbl 1342.68298
Nipkow, Tobias
2
2011
Linear quantifier elimination. Zbl 1207.68339
Nipkow, Tobias
2
2010
Nominal verification of algorithm \(W\). Zbl 1195.68118
Urban, Christian; Nipkow, Tobias
2
2009
Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Zbl 1173.68002
Berghofer, Stefan (ed.); Nipkow, Tobias (ed.); Urban, Christian (ed.); Wenzel, Makarius (ed.)
2
2009
Verifying a hotel key card system. Zbl 1168.68542
Nipkow, Tobias
2
2006
Asserting bytecode safety. Zbl 1108.68432
Wildmoser, Martin; Nipkow, Tobias
2
2005
Prototyping proof carrying code. Zbl 1094.68015
Wildmoser, Martin; Nipkow, Tobias; Klein, Gerwin; Nanz, Sebastian
2
2004
Higher-order algebra, logic, and term rewriting. 1st International Workshop, HOA ’93, Amsterdam, the Netherlands, September 23-24, 1993. Selected papers. Zbl 0825.00070
Heering, Jan (ed.); Meinke, Karl (ed.); Möller, Bernhard (ed.); Nipkow, Tobias (ed.)
2
1994
TYPES ’93, Types for proofs and programs. International Workshop, Nijmegen, the Netherlands, May 24-28, 1993. Selected papers. Zbl 0825.00120
Barendregt, Henk (ed.); Nipkow, Tobias (ed.)
2
1994
Observing nondeterministic data types. Zbl 0665.68013
Nipkow, Tobias
2
1988
Unification in primal algebras. Zbl 0645.68045
Nipkow, Tobias
2
1988
From LCF to Isabelle/HOL. Zbl 1427.68349
Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius
1
2019
Hoare logics for time bounds. A study in meta theory. Zbl 1423.68098
Haslbeck, Maximilian P. L.; Nipkow, Tobias
1
2018
Verified memoization and dynamic programming. Zbl 06947003
Wimmer, Simon; Hu, Shuwei; Nipkow, Tobias
1
2018
Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1420.68049
Traytel, Dmitriy; Nipkow, Tobias
1
2015
Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference. Zbl 1394.68083
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
1
2013
Proving concurrent noninterference. Zbl 1383.68014
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
1
2012
A compiled implementation of normalisation by evaluation. Zbl 1248.68130
Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias
1
2012
Abstract interpretation of annotated commands. Zbl 1360.68762
Nipkow, Tobias
1
2012
Verifying pCTL model checking. Zbl 1352.68154
Hölzl, Johannes; Nipkow, Tobias
1
2012
From LCF to Isabelle/HOL. Zbl 1427.68349
Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius
1
2019
A verified compiler from Isabelle/HOL to CakeML. Zbl 1418.68045
Hupel, Lars; Nipkow, Tobias
4
2018
Verified analysis of random binary tree structures. Zbl 06946981
Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias
2
2018
Hoare logics for time bounds. A study in meta theory. Zbl 1423.68098
Haslbeck, Maximilian P. L.; Nipkow, Tobias
1
2018
Verified memoization and dynamic programming. Zbl 06947003
Wimmer, Simon; Hu, Shuwei; Nipkow, Tobias
1
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
16
2017
Automatic functional correctness proofs for functional search trees. Zbl 06644751
Nipkow, Tobias
4
2016
Amortized complexity verified. Zbl 06481872
Nipkow, Tobias
5
2015
A verified compiler for probability density functions. Zbl 1335.68037
Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias
4
2015
Mining the Archive of Formal Proofs. Zbl 1417.68176
Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias
2
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
29
2014
Unified decision procedures for regular expression equivalence. Zbl 1416.68175
Nipkow, Tobias; Traytel, Dmitriy
5
2014
Data refinement in Isabelle/HOL. Zbl 1317.68212
Haftmann, Florian; Krauss, Alexander; Kunčar, Ondřej; Nipkow, Tobias
17
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
2
2013
Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference. Zbl 1394.68083
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
1
2013
Proof Pearl: regular expression equivalence and relation algebra. Zbl 1269.68090
Krauss, Alexander; Nipkow, Tobias
13
2012
Teaching semantics with a proof assistant: no more LSD trip proofs. Zbl 1325.68005
Nipkow, Tobias
3
2012
Proving concurrent noninterference. Zbl 1383.68014
Popescu, Andrei; Hölzl, Johannes; Nipkow, Tobias
1
2012
A compiled implementation of normalisation by evaluation. Zbl 1248.68130
Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias
1
2012
Abstract interpretation of annotated commands. Zbl 1360.68762
Nipkow, Tobias
1
2012
Verifying pCTL model checking. Zbl 1352.68154
Hölzl, Johannes; Nipkow, Tobias
1
2012
Automatic proof and disproof in Isabelle/HOL. Zbl 1348.68214
Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias
19
2011
Verified efficient enumeration of plane graphs modulo isomorphism. Zbl 1342.68298
Nipkow, Tobias
2
2011
Nitpick: a counterexample generator for higher-order logic based on a relational model finder. Zbl 1291.68326
Blanchette, Jasmin Christian; Nipkow, Tobias
38
2010
Code generation via higher-order rewrite systems. Zbl 1284.68131
Haftmann, Florian; Nipkow, Tobias
38
2010
Sledgehammer: judgement day. Zbl 1291.68327
Böhme, Sascha; Nipkow, Tobias
23
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
14
2010
Linear quantifier elimination. Zbl 1207.68339
Nipkow, Tobias
2
2010
Flyspeck II: The basic linear programs. Zbl 1184.68465
Obua, Steven; Nipkow, Tobias
11
2009
Social choice theory in HOL. Arrow and Gibbard-Satterthwaite. Zbl 1185.68631
Nipkow, Tobias
7
2009
Nominal verification of algorithm \(W\). Zbl 1195.68118
Urban, Christian; Nipkow, Tobias
2
2009
Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Zbl 1173.68002
Berghofer, Stefan (ed.); Nipkow, Tobias (ed.); Urban, Christian (ed.); Wenzel, Makarius (ed.)
2
2009
The Isabelle framework. Zbl 1165.68478
Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias
16
2008
A compiled implementation of normalization by evaluation. Zbl 1165.68442
Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias
5
2008
Linear quantifier elimination. Zbl 1165.68465
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
11
2006
Verifying a hotel key card system. Zbl 1168.68542
Nipkow, Tobias
2
2006
Proving pointer programs in higher-order logic. Zbl 1081.68008
Mehta, Farhad; Nipkow, Tobias
15
2005
Proof pearl: Defining functions over finite sets. Zbl 1152.68529
Nipkow, Tobias; Paulson, Lawrence C.
9
2005
Verifying and reflecting quantifier elimination for Presburger arithmetic. Zbl 1143.03334
Chaieb, Amine; Nipkow, Tobias
4
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
7
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
15
2003
Structured proofs in Isar/HOL. Zbl 1023.68657
Nipkow, Tobias
7
2003
Proving pointer programs in higher-order logic. Zbl 1278.68274
Mehta, Farhad; Nipkow, Tobias
4
2003
Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131
Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus
318
2002
Executing higher order logic. Zbl 1054.68133
Berghofer, Stefan; Nipkow, Tobias
17
2002
Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. Zbl 1064.68543
von Oheimb, David; Nipkow, Tobias
10
2002
Hoare logics for recursive procedures and unbounded nondeterminism. Zbl 1020.03029
Nipkow, Tobias
10
2002
Hoare logics in Isabelle/HOL. Zbl 1097.68632
Nipkow, Tobias
6
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
12
2001
Verified lightweight bytecode verification. Zbl 0997.68018
Klein, Gerwin; Nipkow, Tobias
5
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
Goré, Rajeev (ed.); Leitsch, Alexander (ed.); Nipkow, Tobias (ed.)
4
2001
Proof terms for simply typed higher order logic. Zbl 0974.03013
Berghofer, Stefan; Nipkow, Tobias
6
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
448
1999
HOLCF=HOL+LCF. Zbl 0933.03028
Müller, Olaf; Nipkow, Tobias; von Oheimb, David; Slotosch, Oscar
11
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
26
1998
Winskel is (almost) right: Towards a mechanized semantics textbook. Zbl 0910.68138
Nipkow, Tobias
15
1998
Higher-order rewriting and equational reasoning. Zbl 0970.68081
Nipkow, Tobias; Prehofer, Christian
4
1998
Type reconstruction for type classes. Zbl 0833.68025
Nipkow, Tobias; Prehofer, Christian
4
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
Heering, Jan (ed.); Meinke, Karl (ed.); Möller, Bernhard (ed.); Nipkow, Tobias (ed.)
2
1994
TYPES ’93, Types for proofs and programs. International Workshop, Nijmegen, the Netherlands, May 24-28, 1993. Selected papers. Zbl 0825.00120
Barendregt, Henk (ed.); Nipkow, Tobias (ed.)
2
1994
Orthogonal higher-order rewrite systems are confluent. Zbl 0789.68081
Nipkow, Tobias
12
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
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
17
1989
Equational reasoning in Isabelle. Zbl 0683.68081
Nipkow, Tobias
5
1989
Term rewriting and beyond – theorem proving in Isabelle. Zbl 0694.68059
Nipkow, Tobias
3
1989
Unification in Boolean rings. Zbl 0659.68111
Martin, Ursula; Nipkow, Tobias
6
1988
Observing nondeterministic data types. Zbl 0665.68013
Nipkow, Tobias
2
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
5
1987
Unification in Boolean rings. Zbl 0643.68140
Martin, Ursula; Nipkow, Tobias
7
1986
Non-deterministic data types: Models and implementations. Zbl 0564.68013
Nipkow, Tobias
6
1986
A decidability result about sufficient-completeness of axiomatically specified abstract data types. Zbl 0493.68024
Nipkow, Tobias; Weikum, Gerhard
8
1982
all top 5

Cited by 1,357 Authors

27 Nipkow, Tobias
22 Blanchette, Jasmin Christian
21 Middeldorp, Aart
18 Benzmüller, Christoph Ewald
18 Paulson, Lawrence Charles
18 Thiemann, René
15 Giesl, Jürgen
14 Struth, Georg
13 Ayala-Rincón, Mauricio
13 Lucas, Salvador
13 Nishida, Naoki
12 Popescu, Andrei
12 Vidal, Germán
11 Kaliszyk, Cezary
11 Tinelli, Cesare
11 Zankl, Harald
10 Fernández, Maribel
10 Reynolds, Andrew
9 Guttmann, Walter
9 Lochbihler, Andreas
9 Schmidt-Schauß, Manfred
9 Sternagel, Christian
8 Alpuente, María
8 Kirchner, Claude
8 Moser, Georg
8 Sakai, Masahiko
8 Schneider-Kamp, Peter
8 Zantema, Hans
7 Böhme, Sascha
7 Gabbay, Murdoch James
7 Ghilardi, Silvio
7 Godoy, Guillem
7 Hirokawa, Nao
7 Klein, Gerwin
7 Urban, Christian
7 Vágvölgyi, Sándor
7 van Oostrom, Vincent
7 Wolff, Burkhart
6 Aransay, Jesús
6 Baader, Franz
6 Falaschi, Moreno
6 Felgenhauer, Bertram
6 Foster, Simon
6 Fuhs, Carsten
6 Gao, Xing
6 Guiraud, Yves
6 Guo, Li
6 Kapur, Deepak
6 Kirchner, Hélène
6 Krauss, Alexander
6 Lammich, Peter
6 Meseguer Guaita, José
6 Preoteasa, Viorel
6 Urban, Josef
6 van de Pol, Jan Cornelis
6 Waldmann, Uwe
6 Weber, Tjark
6 Weidenbach, Christoph
6 Woltzenlogel Paleo, Bruno
6 Woodcock, James C. P.
5 Alves, Sandra
5 Antoy, Sergio
5 Avigad, Jeremy
5 Barrett, Clark W.
5 Beringer, Lennart
5 Cain, Alan J.
5 Cavalcanti de Moura, Flávio Leonardo
5 Divasón, Jose
5 Echenim, Mnacho
5 Fleury, Mathias
5 Fontaine, Pascal
5 Giraudo, Samuele
5 Gramlich, Bernhard
5 Haftmann, Florian
5 Kamareddine, Fairouz D.
5 Kesner, Delia
5 Malbos, Philippe
5 Narendran, Paliath
5 Pichardie, David
5 Rabe, Florian
5 Ringeissen, Christophe
5 Traytel, Dmitry
5 Yamada, Akihisa
4 Avanzini, Martin
4 Basin, David A.
4 Baumgartner, Peter
4 Berghammer, Rudolf
4 Blanqui, Frédéric
4 Bulwahn, Lukas
4 Bundy, Alan
4 Cavalcanti, Ana
4 Creus, Carles
4 Dufourd, Jean-François
4 Duggan, Dominic
4 Durán, Francisco
4 Escobar, Santiago
4 Frohn, Florian
4 Genet, Thomas
4 Hales, Thomas Callister
4 Héam, Pierre-Cyrille
...and 1,257 more Authors
all top 5

Cited in 107 Serials

166 Journal of Automated Reasoning
89 Theoretical Computer Science
51 Information and Computation
37 Journal of Symbolic Computation
31 Formal Aspects of Computing
28 Journal of Logical and Algebraic Methods in Programming
19 Information Processing Letters
19 MSCS. Mathematical Structures in Computer Science
16 The Journal of Logic and Algebraic Programming
15 Formal Methods in System Design
14 Journal of Functional Programming
13 Annals of Pure and Applied Logic
13 Logical Methods in Computer Science
12 Annals of Mathematics and Artificial Intelligence
11 Acta Informatica
11 ACM Transactions on Computational Logic
9 Applicable Algebra in Engineering, Communication and Computing
8 Science of Computer Programming
8 Theory and Practice of Logic Programming
8 Mathematics in Computer Science
7 Journal of Applied Logic
6 Journal of Algebra
6 International Journal of Algebra and Computation
5 Journal of Computer and System Sciences
4 Artificial Intelligence
4 Journal of Pure and Applied Algebra
4 Journal of Applied Non-Classical Logics
4 Higher-Order and Symbolic Computation
4 Logica Universalis
3 Discrete Mathematics
3 Algebra Universalis
3 Information Sciences
3 Semigroup Forum
3 Studia Logica
3 Advances in Applied Mathematics
3 International Journal of Foundations of Computer Science
3 Sādhanā
3 Computer Languages, Systems & Structures
3 Journal of Algebra and its Applications
3 Journal of Formalized Reasoning
2 Fuzzy Sets and Systems
2 Programming and Computer Software
2 Synthese
2 New Generation Computing
2 Discrete & Computational Geometry
2 International Journal of Computer Mathematics
2 Journal of Logic, Language and Information
2 RAIRO. Theoretical Informatics and Applications
2 Concurrency and Computation: Practice & Experience
2 The Review of Symbolic Logic
1 Communications in Algebra
1 Communications in Mathematical Physics
1 International Journal of General Systems
1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV)
1 The Mathematical Intelligencer
1 Advances in Mathematics
1 Applied Mathematics and Optimization
1 Journal of Combinatorial Theory. Series A
1 Journal of Mathematical Economics
1 Journal of Philosophical Logic
1 The Journal of Symbolic Logic
1 Mathematische Zeitschrift
1 SIAM Journal on Computing
1 Bulletin of the Section of Logic
1 Topology and its Applications
1 European Journal of Combinatorics
1 Computer Aided Geometric Design
1 Social Choice and Welfare
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 Pattern Recognition
1 Bulletin of the American Mathematical Society. New Series
1 Distributed Computing
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 Theory and Applications of Categories
1 Sbornik: Mathematics
1 Séminaire Lotharingien de Combinatoire
1 Theory of Computing Systems
1 Novi Sad Journal of Mathematics
1 Wuhan University Journal of Natural Sciences (WUJNS)
1 Journal of High Energy Physics
1 Algebraic & Geometric Topology
1 Journal of the Australian Mathematical Society
1 Journal of Systems Science and Complexity
1 Journal of Applied Mathematics
1 JP Journal of Algebra, Number Theory and Applications
1 Journal of Discrete Algorithms
1 Frontiers of Mathematics in China
1 Tbilisi Mathematical Journal
1 Algorithms
1 Symmetry
1 Frontiers of Computer Science
...and 7 more Serials
all top 5

Cited in 39 Fields

948 Computer science (68-XX)
298 Mathematical logic and foundations (03-XX)
27 Category theory; homological algebra (18-XX)
25 Combinatorics (05-XX)
25 General algebraic systems (08-XX)
21 Group theory and generalizations (20-XX)
19 Information and communication theory, circuits (94-XX)
15 Order, lattices, ordered algebraic structures (06-XX)
15 Associative rings and algebras (16-XX)
14 Commutative algebra (13-XX)
9 Numerical analysis (65-XX)
9 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
8 Operations research, mathematical programming (90-XX)
7 General and overarching topics; collections (00-XX)
7 Convex and discrete geometry (52-XX)
5 History and biography (01-XX)
5 Number theory (11-XX)
5 Field theory and polynomials (12-XX)
5 Biology and other natural sciences (92-XX)
4 Linear and multilinear algebra; matrix theory (15-XX)
4 Geometry (51-XX)
4 Mathematics education (97-XX)
3 Nonassociative rings and algebras (17-XX)
3 Probability theory and stochastic processes (60-XX)
3 Systems theory; control (93-XX)
2 Algebraic geometry (14-XX)
2 Ordinary differential equations (34-XX)
2 Operator theory (47-XX)
2 General topology (54-XX)
2 Algebraic topology (55-XX)
2 Mechanics of particles and systems (70-XX)
2 Quantum theory (81-XX)
1 Real functions (26-XX)
1 Several complex variables and analytic spaces (32-XX)
1 Dynamical systems and ergodic theory (37-XX)
1 Calculus of variations and optimal control; optimization (49-XX)
1 Manifolds and cell complexes (57-XX)
1 Fluid mechanics (76-XX)
1 Statistical mechanics, structure of matter (82-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.