Publications

Balazs Toth, Tobias Nipkow. Real-Time Double-Ended Queue Verified (Proof Pearl). In ITP 2023, 2023.

Katahrina Kreuzer, Tobias Nipkow. Verification of NP-hardness Reduction Functions for Exact Lattice Problems. In CADE 29, LNCS, 2023.

Niels Mündler, Tobias Nipkow. A Verified Implementation of B+-Trees in Isabelle/HOL. In Intl. Colloquium on Theoretical Aspects of Computing (ICTAC 2022), Springer, 2022.

Robin Eßmann, Tobias Nipkow, Simon Robillard, Ujkan Sulejmani. Verified Approximation Algorithms. Logical Methods in Computer Science, Volume 18, Issue 1, March 2022.

Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gomez-Londono, Peter Lammich, Christian Sternagel, Simon Wimmer, Bohua Zhan. Functional Algorithms, Verified!. May 2021.

Lukas Stevens, Tobias Nipkow. A Verified Decision Procedure for Orders in Isabelle/HOL. In ATVA 2021, LNCS 12971, Springer, 2021.

Tobias Nipkow, Simon Roßkopf. Isabelle's Metalogic: Formalization and Proof Checker In CADE 28, LNCS, 2021. Best Paper Award.

Tobias Nipkow. Teaching Algorithms and Data Structures with a Proof Assistant (Invited Talk) In Certified Programs and Proofs (CPP 2021), 2021.

Tobias Nipkow, Manuel Eberl, Maximilian P. L. Haslbeck. Verified Textbook Algorithms. A Biased Survey (Invited paper). In ATVA 2020, LNCS, 2020.

Manuel Eberl, Max W. Haslbeck, Tobias Nipkow. Verified Analysis of Random Binary Tree Structures. J. Automated Reasoning, 64(5), 2020.

Robin Eßmann, Tobias Nipkow, Simon Robillard. Verified Approximation Algorithms. In Automated Reasoning (IJCAR 2020), LNCS, 2020.

Martin Rau, Tobias Nipkow. Verification of Closest Pair of Points Algorithms. In Automated Reasoning (IJCAR 2020), LNCS, 2020.

Tobias Nipkow, Thomas Sewell. Proof Pearl: Braun Trees. In Certified Programs and Proofs (CPP 2020), 2020.

Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel. From LCF to Isabelle/HOL. Formal Aspects of Computing, 2019.

Peter Lammich, Tobias Nipkow. Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. In ITP 2019, 2019.

Mohammad Abdulaziz, Kurt Mehlhorn, Tobias Nipkow. Trustworthy Graph Algorithms. In MFCS 2019, 2019.

Tobias Nipkow, Hauke Brinkop. Amortized Complexity Verified. J. Automated Reasoning, 62(3), 2019.

Manuel Eberl, Max W. Haslbeck, Tobias Nipkow. Verified Analysis of Random Binary Tree Structures. In ITP 2018, LNCS, 2018.

Simon Wimmer, Shuwei Hu, Tobias Nipkow. Verified Memoization and Dynamic Programming. In ITP 2018, LNCS, 2018.

Julius Michaelis and Tobias Nipkow. Formalized Proof Systems for Propositional Logic. In Types for Proofs and Programs (TYPES 2017), LIPIcs, 2018.

Lars Hupel, Tobias Nipkow. A Verified Compiler from Isabelle/HOL to CakeML. In European Symposium on Programming (ESOP 2018), LNCS, 2018.

Maximilian Paul Louis Haslbeck, Tobias Nipkow. Hoare Logics for Time Bounds. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), LNCS, 2018.

Tobias Nipkow. Verified Root-Balanced Trees. In Asian Symposium on Programming Languages and Systems, APLAS 2017, LNCS, 2017.

Albert Rizaldi, Jonas Keinholz, Monika Huber, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf, Tobias Nipkow. Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL. In integrated Formal Methods (iFM 2017), LNCS, 2017.

Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi. 5, 2017.

Tobias Nipkow. Automatic Functional Correctness Proofs for Functional Search Trees. In ITP 2016, LNCS, 2016.

Maximilian P.L. Haslbeck, Tobias Nipkow. Verified Analysis of List Update Algorithms. In FSTTCS 2016, 2016.

Dmitriy Traytel, Tobias Nipkow. Verified decision procedures for MSO on words based on derivatives of regular expressions. Journal of Functional Programming, 25, 2015.

Tobias Nipkow. Parameterized Dynamic Tables. 2015.

Tobias Nipkow. Amortized Complexity Verified. In ITP 2015, LNCS, 2015.

Jasmin Blanchette, Max Haslbeck, Daniel Matichuk, Tobias Nipkow. Mining the Archive of Formal Proofs. In Conference on Intelligent Computer Mathematics (CICM 2015), LNCS, 2015.

Manuel Eberl, Johannes Hölzl, Tobias Nipkow. A Verified Compiler for Probability Density Functions. In European Symposium on Programming (ESOP 2015), LNCS, 2015.

Tobias Nipkow, Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014, 298 pages.

Gerwin Klein, Tobias Nipkow. Applications of Interactive Proof to Data Flow Analysis and Security. In Software Systems Safety, 77-134, IOS Press, 2014.

Tobias Nipkow, Dmitriy Traytel. Unified Decision Procedures for Regular Expression Equivalence. In ITP 2014, LNCS, 2014.

Dmitriy Traytel, Tobias Nipkow. A Verified Decision Procedure for MSO on Words Based on Derivatives of Regular Expressions. In International Conference on Functional Programming, 2013.

Andrei Popescu, Johannes Hölzl, Tobias Nipkow. Formalizing Probabilistic Noninterference. In Certified Programs and Proofs (CPP 2013), LNCS, 2013.

Andrei Popescu, Johannes Hölzl, Tobias Nipkow. Formal Verification of Language-Based Concurrent Noninterference. J. Formalized Reasoning, 6:1-30, 2013.

Andrei Popescu, Johannes Hölzl, Tobias Nipkow. Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. In CALCO 2013, LNCS, 2013.

Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow. Data Refinement in Isabelle/HOL. In ITP 2013, LNCS, 2013.

Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus. A Fully Verified Executable LTL Model Checker. In CAV 2013, LNCS, 2013.

Andrei Popescu, Johannes Hölzl, Tobias Nipkow. Proving Concurrent Noninterference. In Certified Programs and Proofs (CPP 2012), LNCS 7679, 2012.

Tobias Nipkow. Abstract Interpretation of Annotated Commands. In Interactive Theorem Proving (ITP 2012), LNCS, 2012.

Tobias Nipkow. Interactive Proof: Introduction to Isabelle/HOL. In Software Safety and Security, IOS Press, 2012.

Johannes Hölzl, Tobias Nipkow. Interactive Verification of Markov Chains: Two Distributed Protocol Case Studies. In Quantities in Formal Methods (QFM 2012), EPTCS 103, 2012.

Johannes Hölzl, Tobias Nipkow. Verifying pCTL Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), LNCS 7214, 2012.

Klaus Aehlig, Florian Haftmann, Tobias Nipkow. A Compiled Implementation of Normalization by Evaluation. Journal of Functional Programming, 22:9-30, 2012.

Tobias Nipkow. Teaching Semantics with a Proof Assistant: No more LSD Trip Proofs (invited paper). In Verification, Model Checking, and Abstract Interpretation (VMCAI 2012), LNCS 7148, 2012.

Dongchen Jiang, Tobias Nipkow. Proof Pearl: The Marriage Theorem. In Certified Programs and Proofs (CPP 2011), LNCS 7068, 2011.

Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow. Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. In Asian Symposium on Programming Languages and Systems (APLAS 2011), LNCS 7078, 2011.

Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow. Automatic Proof and Disproof in Isabelle/HOL (invited paper). In Frontiers of Combining Systems (FroCoS 2011), LNCS 6989, 2011.

Tobias Nipkow. Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. In Interactive Theorem Proving (ITP 2011), LNCS 6898, 2011.

Tobias Nipkow. Majority Vote Algorithm Revisited Again. International Journal of Software and Informatics, 5:21-28, 2011.

Alexander Krauss, Tobias Nipkow. Proof Pearl: Regular Expression Equivalence and Relation Algebra. J. Automated Reasoning 49:95-106, 2012, published online March 2011.

Franz Baader, Bernhard Beckert, Tobias Nipkow. Deduktion: Von der Theorie zur Anwendung. Informatik Spektrum, 33:444-451, 2010.

Tobias Nipkow. Linear Quantifier Elimination. J. Automated Reasoning, 45:189-212, 2010.

Sascha Böhme, Tobias Nipkow. Sledgehammer: Judgement Day. In Automated Reasoning (IJCAR 2010), LNCS 6173, 107-121, 2010.

Jasmin Christian Blanchette, Tobias Nipkow. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In Interactive Theorem Proving (ITP 2010), LNCS 6172, 131-146, 2010.

Florian Haftmann, Tobias Nipkow. Code Generation via Higher-Order Rewrite Systems. In Functional and Logic Programming (FLOPS 2010), LNCS 6009, 103-117, 2010.

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. 44:1-34, 2010.

Steven Obua, Tobias Nipkow. Flyspeck II: the basic linear programs. Annals of Mathematics and Artificial Intelligence. 56:245-272, 2009.

Tobias Nipkow. Social Choice Theory in HOL. Arrow and Gibbard-Satterthwaite. J. Automated Reasoning, 43:289-304, 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.

Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel (Eds). Theorem Proving in Higher-Order Logics (TPHOLs 2009). LNCS 5674, 2009.

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.

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.

Tobias Nipkow. Linear Quantifier Elimination. In Automated Reasoning (IJCAR 2008), LNCS 5195, 18-33, 2008.

Amine Chaieb, Tobias Nipkow. Proof Synthesis and Reflection for Linear Arithmetic. J. Automated Reasoning, 41:33-59, 2008.

Tobias Nipkow. Reflecting Quantifier Elimination for Linear Arithmetic. In Formal Logical Methods for System Security and Correctness, IOS Press, 2008.

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. Verifying a Hotel Key Card System (invited paper). In Theoretical Aspects of Computing (ICTAC 2006), LNCS 4281, 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, Gertrud Bauer, Paula Schultz. Flyspeck I: Tame Graphs. In Automated Reasoning (IJCAR 2006), LNCS 4130, 21-35, 2006.

Gerwin Klein, Tobias Nipkow. A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler. TOPLAS, 28:619-695, 2006.

Amine Chaieb, Tobias Nipkow. Verifying and reflecting quantifier elimination for Presburger arithmetic. In LPAR 2005, LNCS 3835, 367-380, 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.

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.

Martin Wildmoser, Tobias Nipkow. Asserting Bytecode Safety. In European Symposium on Programming (ESOP 2005), LNCS 3444, 326-341, 2005.

Farhad Mehta, Tobias Nipkow. Proving Pointer Programs in Higher-Order Logic. Information and Computation, 199:200-227, 2005.

Stefan Berghofer, Tobias Nipkow. Random Testing in Isabelle/HOL. In Software Engineering and Formal Methods (SEFM 2004), 2004.

Gerwin Klein, Tobias Nipkow. A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler. Tech.Rep., March 2004.

Martin Wildmoser, Tobias Nipkow. Certifying Machine Code Safety: Shallow versus Deep Embedding. In Theorem Proving in Higher Order Logics (TPHOLs 2004), 2004.

Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz. Prototyping Proof-Carrying Code. In Exploring New Frontiers of Theoretical Informatics, 2004.

Tobias Nipkow. Jinja: Towards a Comprehensive Formal Semantics for a Java-like Language. In Proceedings of the Marktoberdorf Summer School 2003, 2006.

Farhad Mehta, Tobias Nipkow. Proving Pointer Programs in Higher-Order Logic. In Automated Deduction - CADE-19, LNCS 2741, 121-135, 2003.

Tobias Nipkow. Structured Proofs in Isar/HOL. In Types for Proofs and Programs (TYPES 2002), LNCS 2646, 259-278, 2003.

Gerwin Klein, Tobias Nipkow. Verified Bytecode Verifiers. Theoretical Computer Science, 298:583-626, 2003.

Tobias Nipkow. Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. In Computer Science Logic (CSL 2002), LNCS 2471, 103-119, 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.

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.

Tobias Nipkow. Hoare Logics in Isabelle/HOL. In Proof and System-Reliability, Kluwer, 2002.

Tobias Nipkow, Lawrence Paulson, Markus Wenzel. Isabelle/HOL. A Proof Assistant for Higher-Order Logic. LNCS 2283, Springer Verlag, 2002, 218 pages.

Stefan Berghofer, Tobias Nipkow. Executing Higher Order Logic. In Types for Proofs and Programs (TYPES 2000), LNCS 2277, 24-40, 2002.

Gerwin Klein, Tobias Nipkow. Verified Lightweight Bytecode Verification. Concurrency and Computation: Practice and Experience, 13:1133-1151, 2001.

Tobias Nipkow. Verified Bytecode Verifiers. In Foundations of Software Science and Computation Structures (FOSSACS 2001), LNCS 2030, 347-363, 2001.

Tobias Nipkow. More Church-Rosser Proofs (in Isabelle/HOL). J. Automated Reasoning, 26:51-66, 2001.

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, David von Oheimb, Cornelia Pusch. microJava: Embedding a Programming Language in a Theorem Prover. In Foundations of Secure Computation, IOS Press, 2000.

Wolfgang Naraschewski, Tobias Nipkow. Type Inference Verified: Algorithm W in Isabelle/HOL. J. Automated Reasoning, 23:299-318, 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.

Olaf Müller, Tobias Nipkow, David von Oheimb, Oscar Slotosch. HOLCF = HOL + LCF. J. Functional Programming, 9:191-223, 1999.

Tobias Nipkow, Leonor Prensa Nieto. Owicki/Gries in Isabelle/HOL. In Fundamental Approaches to Software Engineering (FASE'99), LNCS 1577, 1999, 188-203.

Tobias Nipkow. Winskel is (almost) Right: Towards a Mechanized Semantics Textbook. Formal Aspects of Computing, 10:171-186, 1998.

Tobias Nipkow. Verified Lexical Analysis (invited paper). In Theorem Proving in Higher Order Logics (TPHOLs'98), LNCS 1479, 1998, 1-15.

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, 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 (Ed). Rewriting Techniques and Applications. 9th International Conference, RTA-98. LNCS 1379, 1998.

Franz Baader, Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998, 301 pages.

Richard Mayr, Tobias Nipkow. Higher-Order Rewrite Systems and their Confluence. Theoretical Computer Science, 192:3-29, 1998.

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.

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. Winskel is (almost) Right: Towards a Mechanized Semantics Textbook. In Foundations of Software Technology and Theoretical Computer Science, LNCS 1180, 1996, 180-192.

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.

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.

Tobias Nipkow. More Church-Rosser Proofs (in Isabelle/HOL). In Automated Deduction - CADE-13, LNCS 1104, 1996, 733-747.

Tobias Nipkow, Christian Prehofer. Type Reconstruction for Type Classes. J. Functional Programming, 5(2): 201-224, 1995.

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, Konrad Slind. I/O Automata in Isabelle/HOL. In Types for Proofs and Programs, LNCS 996, 1995, 101-119.

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.

Zhenyu Qian, Tobias Nipkow. Reduction and Unification in Lambda Calculi with a General Notion of Subtype. J. Automated Reasoning, 12:389-406, 1994.

Lawrence C. Paulson (with contributions by Tobias Nipkow). Isabelle: A Generic Theorem Prover. LNCS 828, 1994.

J. Heering, K. Meinke, B. Möller, T. Nipkow (Eds). Higher-Order Algebra, Logic and Term Rewriting, LNCS 816, 1994.

Henk Barendregt, Tobias Nipkow (Eds). Types for Proofs and Programs. LNCS 806, 1994.

Tobias Nipkow. Functional Unification of Higher-Order Patterns. In Proc. 8th IEEE Symp. Logic in Computer Science, IEEE Press (1993), 64-74.

Tobias Nipkow. Orthogonal Higher-Order Rewrite Systems are Confluent. In Proc. Int. Conf. Typed Lambda Calculi and Applications, LNCS 664 (1993), 306-317.

Tobias Nipkow, Christian Prehofer. Type Checking Type Classes. In Proc. 20th ACM Symp. Principles of Programming Languages, ACM Press (1993), 409-418.

Tobias Nipkow. Order-Sorted Polymorphism in Isabelle. In Logical Environments, Cambridge University Press (1993), 164-188.

Tobias Nipkow, Zhenyu Qian. Reduction and Unification in Lambda Calculi with Subtypes. In Proc. 11th Int. Conf. Automated Deduction, LNCS 607 (1992), 66-78.

Tobias Nipkow. Combining Matching Algorithms: The Regular Case. J. Symbolic Computation, 12(6):633-653, 1991.

Tobias Nipkow, Gregor Snelting. Type Classes and Overloading Resolution via Order-Sorted Unification. In Proc. 5th ACM Conf. Functional Programming Languages and Computer Architecture, LNCS 523 (1991), 1-14.

Tobias Nipkow. Higher-Order Critical Pairs. In Proc. 6th IEEE Symp. Logic in Computer Science, IEEE Press (1991), 342-349.

Tobias Nipkow, Zhenyu Qian. Modular Higher-Order E-Unification. In Proc. 4th Int. Conf. Rewriting Techniques and Applications, LNCS 488 (1991), 200-214.

Tobias Nipkow. Constructive Rewriting. Computer Journal, 34:34-41, 1991.

Ursula Martin, Tobias Nipkow. Ordered Rewriting and Confluence. In Proc. 10th Int. Conf. Automated Deduction, LNCS 449 (1990), 366-380.

Tobias Nipkow. Higher-Order Unification, Polymorphism and Subsorts. In Proc. 2nd Int. Workshop Conditional and Typed Rewriting Systems, LNCS 516 (1990).

Tobias Nipkow. Proof Transformations for Equational Theories. In Proc. 5th IEEE Symp. Logic in Computer Science, IEEE Press (1990), 278-288.

Ursula Martin, Tobias Nipkow. Automating Squiggol. In Programming Concepts and Methods, North-Holland (1990), 233-247.

Tobias Nipkow. Formal Verification of Data Type Refinement - Theory and Practice. In Stepwise Refinement of Distributed Systems, LNCS 430 (1990), 561-591.

Tobias Nipkow. Unification in Primal Algebras, Their Powers and Their Varieties. J. ACM, 37:742-776, 1990.

Tobias Nipkow. Term Rewriting and Beyond - Theorem Proving in Isabelle. Formal Aspects of Computing,1:320-338, 1989.

Tobias Nipkow. Equational Reasoning in Isabelle. Science of Computer Programming, 12:123-149, 1989.

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

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. Observing Nondeterministic Data Types. In D. Sannella and A. Tarlecki, editors, Recent Trends in Data Type Specification, LNCS 332, (1988), 170-183.

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

Ursula Martin, Tobias Nipkow. Boolean Unification. J. Automated Reasoning, 4:381-396, 1988.

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)

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

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. Non-Deterministic Data Types: Models and Implementations. Acta Informatica, 22:629-661, 1986.

Tobias Nipkow, Gerhard Weikum. A Decidability Result about Sufficient-Completeness of Axiomatically Specified Abstract Data Types. In Proc. 6th GI-Conf. Theoretical Computer Science, LNCS 145, 1983.