| 2026 | IJCAR | A Unified Formalization of Context-Free Grammar Theory. | Tobias Nipkow, Fabian Lehr, Moritz Roos, Akihisa Yamada |
| 2025 | CADE | Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL. | Lukas Bartl, Jasmin Blanchette, Tobias Nipkow |
| 2024 | ITP | Alpha-Beta Pruning Verified (Invited Talk). | Tobias Nipkow |
| 2024 | ITP | A Verified Earley Parser. | Martin Rau, Tobias Nipkow |
| 2023 | CADE | Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. | Katharina Kreuzer, Tobias Nipkow |
| 2023 | ITP | Real-Time Double-Ended Queue Verified (Proof Pearl). | Balzs Tth, Tobias Nipkow |
| 2022 | ICTAC | A Verified Implementation of B | Niels Mndler, Tobias Nipkow |
| 2021 | ATVA | A Verified Decision Procedure for Orders in Isabelle/HOL. | Lukas Stevens, Tobias Nipkow |
| 2021 | CADE | Isabelle's Metalogic: Formalization and Proof Checker. | Tobias Nipkow, Simon Rokopf |
| 2021 | CPP | Teaching algorithms and data structures with a proof assistant (invited talk). | Tobias Nipkow |
| 2020 | ATVA | Verified Textbook Algorithms - A Biased Survey. | Tobias Nipkow, Manuel Eberl, Maximilian P. L. Haslbeck |
| 2020 | CADE | Verified Approximation Algorithms. | Robin Emann, Tobias Nipkow, Simon Robillard |
| 2020 | CADE | Verification of Closest Pair of Points Algorithms. | Martin Rau, Tobias Nipkow |
| 2020 | CPP | Proof pearl: Braun trees. | Tobias Nipkow, Thomas Sewell |
| 2019 | ITP | Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. | Peter Lammich, Tobias Nipkow |
| 2019 | MFCS | Trustworthy Graph Algorithms (Invited Talk). | Mohammad Abdulaziz, Kurt Mehlhorn, Tobias Nipkow |
| 2018 | ESOP | A Verified Compiler from Isabelle/HOL to CakeML. | Lars Hupel, Tobias Nipkow |
| 2018 | ITP | Verified Analysis of Random Binary Tree Structures. | Manuel Eberl, Max W. Haslbeck, Tobias Nipkow |
| 2018 | ITP | Verified Memoization and Dynamic Programming. | Simon Wimmer, Shuwei Hu, Tobias Nipkow |
| 2018 | TACAS | Hoare Logics for Time Bounds - A Study in Meta Theory. | Maximilian P. L. Haslbeck, Tobias Nipkow |
| 2017 | APLAS | Verified Root-Balanced Trees. | Tobias Nipkow |
| 2017 | IFM | Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL. | Albert Rizaldi, Jonas Keinholz, Monika Huber, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf, Tobias Nipkow |
| 2016 | ITP | Automatic Functional Correctness Proofs for Functional Search Trees. | Tobias Nipkow |
| 2015 | ESOP | A Verified Compiler for Probability Density Functions. | Manuel Eberl, Johannes Hlzl, Tobias Nipkow |
| 2015 | ITP | Amortized Complexity Verified. | Tobias Nipkow |
| 2014 | HASKELL | Experience report: the next 1100 Haskell programmers. | Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel |
| 2014 | ITP | Unified Decision Procedures for Regular Expression Equivalence. | Tobias Nipkow, Dmitriy Traytel |
| 2013 | CALCO | Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2013 | CAV | A Fully Verified Executable LTL Model Checker. | Javier Esparza, Peter Lammich, Ren Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus |
| 2013 | CPP | Formalizing Probabilistic Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2013 | ICFP | Verified decision procedures for MSO on words based on derivatives of regular expressions. | Dmitriy Traytel, Tobias Nipkow |
| 2013 | ITP | Data Refinement in Isabelle/HOL. | Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow |
| 2013 | TABLEAUX | A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions. | Tobias Nipkow, Maximilian P. L. Haslbeck |
| 2012 | CPP | Proving Concurrent Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2012 | ITP | Abstract Interpretation of Annotated Commands. | Tobias Nipkow |
| 2012 | TACAS | Verifying pCTL Model Checking. | Johannes Hlzl, Tobias Nipkow |
| 2012 | VMCAI | Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs. | Tobias Nipkow |
| 2011 | APLAS | Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. | Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow |
| 2011 | CPP | Proof Pearl: The Marriage Theorem. | Dongchen Jiang, Tobias Nipkow |
| 2011 | ITP | Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. | Tobias Nipkow |
| 2010 | CADE | Sledgehammer: Judgement Day. | Sascha Bhme, Tobias Nipkow |
| 2010 | FLOPS | Code Generation via Higher-Order Rewrite Systems. | Florian Haftmann, Tobias Nipkow |
| 2010 | ITP | Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. | Jasmin Christian Blanchette, Tobias Nipkow |
| 2008 | CADE | Linear Quantifier Elimination. | Tobias Nipkow |
| 2007 | CADE | Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic. | Tobias Nipkow |
| 2006 | CADE | Flyspeck I: Tame Graphs. | Tobias Nipkow, Gertrud Bauer, Paula Schultz |
| 2006 | ICTAC | Verifying a Hotel Key Card System. | Tobias Nipkow |
| 2006 | OOPSLA | An operational semantics and type safety prooffor multiple inheritance in C++. | Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip |
| 2005 | ESOP | Asserting Bytecode Safety. | Martin Wildmoser, Tobias Nipkow |
| 2005 | LPAR | Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. | Amine Chaieb, Tobias Nipkow |
| 2004 | SEFM | Random Testing in Isabelle/HOL. | Stefan Berghofer, Tobias Nipkow |
| 2003 | CADE | Proving Pointer Programs in Higher-Order Logic. | Farhad Mehta, Tobias Nipkow |
| 2002 | CSL | Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. | Tobias Nipkow |
| 2002 | FM | Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. | David von Oheimb, Tobias Nipkow |
| 2001 | FOSSACS | Verified Bytecode Verifiers. | Tobias Nipkow |
| 2000 | GI | Workshop ber Rigorose Entwicklung software-intensiver Systeme. | Martin Wirsing, Martin Gogolla, Hans-Jrg Kreowski, Tobias Nipkow, Wolfgang Reif |
| 1999 | CADE | Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract). | Tobias Nipkow |
| 1999 | FASE | Owicki/Gries in Isabelle/HOL. | Tobias Nipkow, Leonor Prensa Nieto |
| 1998 | POPL | Java | Tobias Nipkow, David von Oheimb |
| 1996 | CADE | More Church-Rosser Proofs (in Isabelle/HOL). | Tobias Nipkow |
| 1995 | TACAS | Combining Model Checking and Deduction for I/O-Automata. | Olaf Mller, Tobias Nipkow |
| 1993 | LICS | Functional Unification of Higher-Order Patterns | Tobias Nipkow |
| 1993 | POPL | Type Checking Type Classes. | Tobias Nipkow, Christian Prehofer |
| 1992 | CADE | Isabelle-91. | Tobias Nipkow, Lawrence C. Paulson |
| 1992 | CADE | Reduction and Unification in Lambda Calculi with Subtypes. | Tobias Nipkow, Zhenyu Qian |
| 1991 | LICS | Higher-Order Critical Pairs | Tobias Nipkow |
| 1990 | CADE | Ordered Rewriting and Confluence. | Ursula Martin, Tobias Nipkow |
| 1990 | LICS | Proof Transformations for Equational Theories | Tobias Nipkow |
| 1987 | STACS | Are Homomorphisms Sufficient for Behavioural Implementations of Deterministic and Nondeterministic Data Types? | Tobias Nipkow |
| 1986 | CADE | Unification in Boolean Rings. | Ursula Martin, Tobias Nipkow |