Tobias Nipkow, Gerhard Weikum. A Decidability Result about Sufficient-Completeness of Axiomatically Specified Abstract Data Types. In A.B. Cremers and H.P. Kriegel, editors, Proc. 6th GI-Conf. Theoretical Computer Science, LNCS 145 (1983), 257-268.
Tobias Nipkow. Non-Deterministic Data Types: Models and Implementations. Acta Informatica, 22:629-661, 1986.
Ursula Martin, Tobias Nipkow. Unification in Boolean Rings. In J. Siekmann, editor, Proc. 8th Int. Conf. Automated Deduction, LNCS 230 (1986), 506-513. SpringerLink
Tobias Nipkow. Are Homomorphisms Sufficient for Behavioural Implementations of Deterministic and Nondeterministic Data Types? In F.J. Brandenburg and G. Vidal-Naquet and M. Wirsing, editors, Proc. 4th Symp. Theoretical Aspects of Computer Science, LNCS 247 (1987), 260-271. SpringerLink
Tobias Nipkow. Behavioural Implementation Concepts for Nondeterministic Data Types. Ph.D. thesis, University of Manchester, 1987. (Appeared as Report UMCS-87-5-3, Dept. of Computer Science, University of Manchester)
Ursula Martin, Tobias Nipkow. Boolean Unification. J. Automated Reasoning, 4:381-396, 1988.
Tobias Nipkow. Unification in Primal Algebras. In M. Dauchet and M. Nivat, editors, Proc. 13th Coll. Trees in Algebra and Programming, LNCS 299 (1988), 117-131. SpringerLink
Tobias Nipkow. Observing Nondeterministic Data Types. In D. Sannella and A. Tarlecki, editors, Recent Trends in Data Type Specification, LNCS 332, (1988), 170-183.
Ursula Martin, Tobias Nipkow. Boolean Unification - The Story So Far. J. Symbolic Computation, 7:275-293, 1989. Reprinted in C. Kirchner, editor, Unification, Academic Press (1990), 437-455.
Tobias Nipkow. Combining Matching Algorithms: The Regular Case. In N. Dershowitz, editor, Proc. 3rd Int. Conf. Rewriting Techniques and Applications, LNCS 355 (1989), 343-358. SpringerLink
Tobias Nipkow. Equational Reasoning in Isabelle. Science of Computer Programming, 12:123-149, 1989.
Tobias Nipkow. Term Rewriting and Beyond - Theorem Proving in Isabelle. Formal Aspects of Computing,1:320-338, 1989.
Tobias Nipkow. Unification in Primal Algebras, Their Powers and Their Varieties. J. ACM, 37:742-776, 1990.
Tobias Nipkow. Formal Verification of Data Type Refinement - Theory and Practice. In J.W. de Bakker and W.-P. de Roever and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, LNCS 430 (1990), 561-591.
Ursula Martin, Tobias Nipkow. Automating Squiggol. In M. Broy and C.B. Jones, editors, Programming Concepts and Methods, North-Holland (1990), 233-247.
Tobias Nipkow. Proof Transformations for Equational Theories. In Proc. 5th IEEE Symp. Logic in Computer Science, IEEE Press (1990), 278-288.
Tobias Nipkow. Higher-Order Unification, Polymorphism and Subsorts. In S. Kaplan and M. Okada, editors, Proc. 2nd Int. Workshop Conditional and Typed Rewriting Systems, LNCS 516 (1990).
Ursula Martin, Tobias Nipkow. Ordered Rewriting and Confluence. In M.E. Stickel, editor, Proc. 10th Int. Conf. Automated Deduction, LNCS 449 (1990), 366-380.
Tobias Nipkow. Constructive Rewriting. Computer Journal,34:34-41, 1991.
Tobias Nipkow, Zhenyu Qian. Modular Higher-Order E-Unification. In R.V. Book, editor, Proc. 4th Int. Conf. Rewriting Techniques and Applications, LNCS 488 (1991), 200-214.
Tobias Nipkow. Higher-Order Critical Pairs. In Proc. 6th IEEE Symp. Logic in Computer Science, IEEE Press (1991), 342-349.
Tobias Nipkow, Gregor Snelting. Type Classes and Overloading Resolution via Order-Sorted Unification. In J. Hughes, editor, Proc. 5th ACM Conf. Functional Programming Languages and Computer Architecture, LNCS 523 (1991), 1-14.
Tobias Nipkow. Combining Matching Algorithms: The Regular Case. J. Symbolic Computation, 12(6):633-653, 1991.
Tobias Nipkow, Zhenyu Qian. Reduction and Unification in Lambda Calculi with Subtypes. In D. Kapur, editor, Proc. 11th Int. Conf. Automated Deduction, LNCS 607 (1992), 66-78.
Tobias Nipkow. Order-Sorted Polymorphism in Isabelle. In G. Huet and G. Plotkin, editors, Logical Environments, Cambridge University Press (1993), 164-188.
Tobias Nipkow, Christian Prehofer. Type Checking Type Classes. In Proc. 20th ACM Symp. Principles of Programming Languages, ACM Press (1993), 409-418.
Tobias Nipkow. Orthogonal Higher-Order Rewrite Systems are Confluent. In M. Bezem and J.F. Groote, editors, Proc. Int. Conf. Typed Lambda Calculi and Applications, LNCS 664 (1993), 306-317.
Tobias Nipkow. Functional Unification of Higher-Order Patterns. In Proc. 8th IEEE Symp. Logic in Computer Science, IEEE Press (1993), 64-74.
Henk Barendregt, Tobias Nipkow (Eds). Types for Proofs and Programs. LNCS 806, 1994.
J. Heering, K. Meinke, B. Möller, T. Nipkow (Eds). Higher-Order Algebra, Logic and Term Rewriting, LNCS 816, 1994.
Lawrence C. Paulson (with contributions by Tobias Nipkow). Isabelle: A Generic Theorem Prover. LNCS 828, 1994.
Zhenyu Qian, Tobias Nipkow. Reduction and Unification in Lambda Calculi with a General Notion of Subtype, J. Automated Reasoning, 12:389-406, 1994.
Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, Birgit Schieder. Interpreter Verification for a Functional Language. In Proc. 14th Conf. Foundations of Software Technology and Theoretical Computer Science, LNCS 880, 1994, 77-88.
Tobias Nipkow, Konrad Slind. I/O Automata in Isabelle/HOL. In Types for Proofs and Programs, LNCS 996, 1995, 101-119.
Olaf Müller, Tobias Nipkow. Combining Model Checking and Deduction for I/O-Automata. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019, 1995, 1-16.
Tobias Nipkow, Christian Prehofer. Type Reconstruction for Type Classes. J. Functional Programming, 5(2): 201-224, 1995.
Tobias Nipkow. More Church-Rosser Proofs (in Isabelle/HOL). In Automated Deduction - CADE-13, LNCS 1104, 1996, 733-747.
Dieter Nazareth, Tobias Nipkow. Formal Verification of Algorithm W: The Monomorphic Case. In Theorem Proving in Higher Order Logics (TPHOLs'96), LNCS 1125, 1996, 331-346.
Wolfgang Naraschewski, Tobias Nipkow. Type Inference Verified: Algorithm W in Isabelle/HOL. In Types for Proofs and Programs: Intl. Workshop TYPES '96, LNCS 1512, 1998, 317-332.
Tobias Nipkow. Winskel is (almost) Right: Towards a Mechanized Semantics Textbook. In Foundations of Software Technology and Theoretical Computer Science, LNCS 1180, 1996, 180-192.
Olaf Müller, Tobias Nipkow. Traces of I/O Automata in Isabelle/HOLCF. In TAPSOFT'97: Theory and Practice of Software Development, LNCS 1214, 1997, 580-594.
Tobias Nipkow, David von Oheimb. Java-light is Type-Safe - Definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, ACM Press, 1998, 161-170.
Richard Mayr, Tobias Nipkow. Higher-Order Rewrite Systems and their Confluence. Theoretical Computer Science, 192:3-29, 1998.
Franz Baader, Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998, 301 pages.
Tobias Nipkow (Ed). Rewriting Techniques and Applications. 9th International Conference, RTA-98. LNCS 1379, 1998.
Tobias Nipkow, Christian Prehofer. Higher-Order Rewriting and Equational Reasoning. In: W. Bibel, P. Schmitt (eds.). Automated Deduction - A Basis for Applications. Volume I. Kluwer, 1998, 399-430.
Tobias Nipkow, Wolfgang Reif. Introduction to Part One, Interactive Theorem Proving. In: W. Bibel, P. Schmitt (eds.). Automated Deduction - A Basis for Applications. Volume II. Kluwer, 1998, 3-11.
Tobias Nipkow. Verified Lexical Analysis (invited paper). In Theorem Proving in Higher Order Logics (TPHOLs'98), LNCS 1479, 1998, 1-15.
Tobias Nipkow. Winskel is (almost) Right: Towards a Mechanized Semantics Textbook. Formal Aspects of Computing, 10:171-186, 1998.
Tobias Nipkow, Leonor Prensa Nieto. Owicki/Gries in Isabelle/HOL. In Fundamental Approaches to Software Engineering (FASE'99), LNCS 1577, 1999, 188-203.
Olaf Müller, Tobias Nipkow, David von Oheimb, Oscar Slotosch. HOLCF = HOL + LCF. J. Functional Programming, 9:191-223, 1999.
David von Oheimb, Tobias Nipkow. Machine-Checking the Java Specification: Proving Type-Safety. In Formal Syntax and Semantics of Java, LNCS 1523, 1999, 119-156.
Wolfgang Naraschewski, Tobias Nipkow. Type Inference Verified: Algorithm W in Isabelle/HOL. J. Automated Reasoning, 23:299-318, 1999.
Tobias Nipkow, David von Oheimb, Cornelia Pusch. microJava: Embedding a Programming Language in a Theorem Prover. In Foundations of Secure Computation, IOS Press, 2000.
Stefan Berghofer, Tobias Nipkow. Proof terms for simply typed higher order logic. In Theorem Proving in Higher Order Logics (TPHOLs 2000), LNCS 1869, 2000.
Tobias Nipkow. More Church-Rosser Proofs (in Isabelle/HOL). J. Automated Reasoning, 26:51-66, 2001.
Tobias Nipkow. Verified Bytecode Verifiers. In Foundations of Software Science and Computation Structures (FOSSACS 2001), LNCS 2030, 347-363, 2001.
Gerwin Klein, Tobias Nipkow. Verified Lightweight Bytecode Verification. Concurrency and Computation: Practice and Experience, 13:1133-1151, 2001.
Stefan Berghofer, Tobias Nipkow. Executing Higher Order Logic. In Types for Proofs and Programs (TYPES 2000), LNCS 2277, 24-40, 2002.
Tobias Nipkow, Lawrence Paulson, Markus Wenzel. Isabelle/HOL. A Proof Assistant for Higher-Order Logic. LNCS 2283, Springer Verlag, 2002, 218 pages.
Tobias Nipkow. Hoare Logics in Isabelle/HOL. In Proof and System-Reliability, Kluwer, 2002.
David von Oheimb, Tobias Nipkow. Hoare Logic for NanoJava: Auxiliary Variables, Side Effects and Virtual Methods Revisited. In Formal Methods Europe (FME 2002), LNCS 2391, 89-105, 2002.
Gertrud Bauer, Tobias Nipkow. The 5 Colour Theorem in Isabelle/Isar. In Theorem Proving in Higher Order Logics (TPHOLs 2002), LNCS 2410, 67-82, 2002.
Tobias Nipkow. Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. In Computer Science Logic (CSL 2002), LNCS 2471, 103-119, 2002.
Gerwin Klein, Tobias Nipkow. Verified Bytecode Verifiers. Theoretical Computer Science, 298:583-626, 2003.
Tobias Nipkow. Structured Proofs in Isar/HOL. In Types for Proofs and Programs (TYPES 2002), LNCS 2646, 259-278, 2003.
Farhad Mehta, Tobias Nipkow. Proving Pointer Programs in Higher-Order Logic. In Automated Deduction - CADE-19, LNCS 2741, 121-135, 2003.
Tobias Nipkow. Jinja: Towards a Comprehensive Formal Semantics for a Java-like Language. In Proceedings of the Marktoberdorf Summer School 2003, 2006.
Amine Chaieb, Tobias Nipkow. Generic proof synthesis for Presburger arithmetic Tech.Rep., October 2003.
Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz. Prototyping Proof-Carrying Code. In Exploring New Frontiers of Theoretical Informatics, 2004.
Martin Wildmoser, Tobias Nipkow. Certifying Machine Code Safety: Shallow versus Deep Embedding. In Theorem Proving in Higher Order Logics (TPHOLs 2004), 2004.
Gerwin Klein, Tobias Nipkow. A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler. Tech.Rep., March 2004.
Stefan Berghofer, Tobias Nipkow. Random Testing in Isabelle/HOL. In Software Engineering and Formal Methods (SEFM 2004), 2004.
Farhad Mehta, Tobias Nipkow. Proving Pointer Programs in Higher-Order Logic. Information and Computation, 199:200-227, 2005.
Martin Wildmoser, Tobias Nipkow. Asserting Bytecode Safety. In European Symposium on Programming (ESOP 2005), LNCS 3444, 326-341, 2005.
Martin Wildmoser, Amine Chaieb, Tobias Nipkow. Bytecode Analysis for Proof Carrying Code. In Proceedings of the First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2005), Electronic Notes in Computer Science (ENTCS), Volume 141, Issue 1, 2005.
Tobias Nipkow, Lawrence C. Paulson. Proof Pearl: Defining Functions Over Finite Sets. In Theorem Proving in Higher Order Logics (TPHOLs 2005), LNCS 3603, 285-396, 2005.
Amine Chaieb, Tobias Nipkow. Verifying and reflecting quantifier elimination for Presburger arithmetic. In LPAR 2005, LNCS 3835, 367-380, 2005.
Gerwin Klein, Tobias Nipkow. A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler. TOPLAS, 28:619-695, 2006.
Tobias Nipkow, Gertrud Bauer, Paula Schultz. Flyspeck I: Tame Graphs. In Automated Reasoning (IJCAR 2006), LNCS 4130, 21-35, 2006.
Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip. An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++. In OOPSLA 2006.
Tobias Nipkow. Verifying a Hotel Key Card System (invited paper). In Theoretical Aspects of Computing (ICTAC 2006), LNCS 4281, 2006.
Lukas Bulwahn, Alexander Krauss, Tobias Nipkow. Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. In Theorem Proving in Higher Order Logics (TPHOLs 2007), LNCS 4732, 38-53, 2007.
Tobias Nipkow. Reflecting Quantifier Elimination for Linear Arithmetic. In Formal Logical Methods for System Security and Correctness, IOS Press, 2008.
Amine Chaieb, Tobias Nipkow. Proof Synthesis and Reflection for Linear Arithmetic. J. Automated Reasoning, 41:33-59, 2008.
Tobias Nipkow. Linear Quantifier Elimination. In Automated Reasoning (IJCAR 2008), LNCS 5195, 18-33, 2008.
Makarius Wenzel, Lawrence Paulson, Tobias Nipkow. The Isabelle Framework (Invited Tutorial). In Theorem Proving in Higher Order Logics (TPHOLs 2008), LNCS 5170, 33-38, 2008.
Klaus Aehlig, Florian Haftmann, Tobias Nipkow. A Compiled Implementation of Normalization by Evaluation. In Theorem Proving in Higher Order Logics (TPHOLs 2008), LNCS 5170, 39-54, 2008.
Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel (Eds). Theorem Proving in Higher-Order Logics (TPHOLs 2009), LNCS 5674, 2009.
Christian Urban, Tobias Nipkow. Nominal verification of algorithm W. In From Semantics to Computer Science. Essays in Honour of Gilles Kahn. Cambridge University Press, 363-382, 2009.
Tobias Nipkow. Social Choice Theory in HOL. Arrow and Gibbard-Satterthwaite. J. Automated Reasoning, 43:289-304, 2009.
Steven Obua, Tobias Nipkow. Flyspeck II: the basic linear programs. Annals of Mathematics and Artificial Intelligence. Online Nov. 2009.
Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller. A Revision of the Proof of the Kepler Conjecture. Discrete and Computational Geometry. Online Mar. 2009.
Florian Haftmann, Tobias Nipkow. Code Generation via Higher-Order Rewrite Systems. In Functional and Logic Programming (FLOPS 2010), LNCS, ?-?, 2010.
Sascha Böhme, Tobias Nipkow. Sledgehammer: Judgement Day. In Automated Reasoning (IJCAR 2010), LNCS ?, ?-?, 2010.