Tobias Nipkow - RankMe

235 papers A* 6A 22B 34C 5Misc 1Journal 106Unranked 46

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Context-Free Grammars and Languages. Arch. Formal Proofs Tobias Nipkow, Markus Gschoßmann, Felix Krayer, Fabian Lehr, Bruno Philipp, August Martin Stimpfle, Kaan Taskin, Akihisa Yamada
2025	J	`jnl`	Dyck Language. Arch. Formal Proofs Tobias Nipkow, Moritz Roos
2025	A	`conf`	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL. CADE Lukas Bartl, Jasmin Blanchette, Tobias Nipkow
2025	J	`jnl`	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL. CoRR Lukas Bartl, Jasmin Blanchette, Tobias Nipkow
2025	J	`jnl`	Greibach Normal Form. Arch. Formal Proofs Alexander Haberl, Tobias Nipkow, Akihisa Yamada
2025	J	`jnl`	Power Operator for Lists. Arch. Formal Proofs Stepan Holub, Martin Raska, Stepán Starosta, Tobias Nipkow
2025	J	`jnl`	Pre*: The Predecessors of a Regular Language w.r.t. a Context-Free Grammar, with Applications. Arch. Formal Proofs Tassilo Lemke, Tobias Nipkow
2025	J	`jnl`	Pushdown Automata. Arch. Formal Proofs Kaan Taskin, Tobias Nipkow
2025	J	`jnl`	Two-Way Deterministic Finite Automata. Arch. Formal Proofs Felipe Escallón, Tobias Nipkow
2024	—	`ch.`	A Note on Proofs of Earley's Recognizer. The Practice of Formal Methods (II) Tobias Nipkow, Martin Rau
2024	B	`conf`	A Verified Earley Parser. ITP Martin Rau, Tobias Nipkow
2024	B	`conf`	Alpha-Beta Pruning Verified (Invited Talk). ITP Tobias Nipkow
2024	J	`jnl`	Alpha-Beta Pruning. Arch. Formal Proofs Tobias Nipkow
2024	J	`jnl`	Gale-Shapley Verified. J. Autom. Reason. Tobias Nipkow
2024	—	`conf`	Region Quadtrees Verified. Taming the Infinities of Concurrency Tobias Nipkow
2024	J	`jnl`	Region Quadtrees. Arch. Formal Proofs Tobias Nipkow
2023	J	`jnl`	A Formalization and Proof Checker for Isabelle's Metalogic. J. Autom. Reason. Simon Roßkopf, Tobias Nipkow
2023	B	`conf`	Real-Time Double-Ended Queue Verified (Proof Pearl). ITP Balázs Tóth, Tobias Nipkow
2023	A	`conf`	Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. CADE Katharina Kreuzer, Tobias Nipkow
2023	J	`jnl`	Verification of NP-hardness Reduction Functions for Exact Lattice Problems. CoRR Katharina Kreuzer, Tobias Nipkow
2022	C	`conf`	A Verified Implementation of B ICTAC Niels Mündler, Tobias Nipkow
2022	J	`jnl`	A Verified Implementation of B+-Trees in Isabelle/HOL. CoRR Niels Mündler, Tobias Nipkow
2022	J	`jnl`	Real-Time Double-Ended Queue. Arch. Formal Proofs Balázs Tóth, Tobias Nipkow
2022	J	`jnl`	Verified Approximation Algorithms. Log. Methods Comput. Sci. Robin Eßmann, Tobias Nipkow, Simon Robillard, Ujkan Sulejmani
2021	B	`conf`	A Verified Decision Procedure for Orders in Isabelle/HOL. ATVA Lukas Stevens, Tobias Nipkow
2021	J	`jnl`	A Verified Decision Procedure for Orders in Isabelle/HOL. CoRR Lukas Stevens, Tobias Nipkow
2021	J	`jnl`	Gale-Shapley Algorithm. Arch. Formal Proofs Tobias Nipkow
2021	A	`conf`	Isabelle's Metalogic: Formalization and Proof Checker. CADE Tobias Nipkow, Simon Roßkopf
2021	J	`jnl`	Isabelle's Metalogic: Formalization and Proof Checker. Arch. Formal Proofs Tobias Nipkow, Simon Roßkopf
2021	J	`jnl`	Isabelle's Metalogic: Formalization and Proof Checker. CoRR Tobias Nipkow, Simon Roßkopf
2021	B	`conf`	Teaching algorithms and data structures with a proof assistant (invited talk). CPP Tobias Nipkow
2021	J	`jnl`	Verified Approximation Algorithms. CoRR Robin Eßmann, Tobias Nipkow, Simon Robillard
2020	J	`jnl`	Closest Pair of Points Algorithms. Arch. Formal Proofs Martin Rau, Tobias Nipkow
2020	B	`conf`	Proof pearl: Braun trees. CPP Tobias Nipkow, Thomas Sewell
2020	—	`conf`	Verification of Closest Pair of Points Algorithms. IJCAR (2) Martin Rau, Tobias Nipkow
2020	J	`jnl`	Verified Analysis of Random Binary Tree Structures. J. Autom. Reason. Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
2020	—	`conf`	Verified Approximation Algorithms. IJCAR (2) Robin Eßmann, Tobias Nipkow, Simon Robillard
2020	J	`jnl`	Verified Approximation Algorithms. Arch. Formal Proofs Robin Eßmann, Tobias Nipkow, Simon Robillard
2020	B	`conf`	Verified Textbook Algorithms - A Biased Survey. ATVA Tobias Nipkow, Manuel Eberl, Maximilian P. L. Haslbeck
2019	J	`jnl`	Amortized Complexity Verified. J. Autom. Reason. Tobias Nipkow, Hauke Brinkop
2019	J	`jnl`	From LCF to Isabelle/HOL. CoRR Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel
2019	J	`jnl`	From LCF to Isabelle/HOL. Formal Aspects Comput. Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel
2019	J	`jnl`	Priority Search Trees. Arch. Formal Proofs Peter Lammich, Tobias Nipkow
2019	B	`conf`	Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. ITP Peter Lammich, Tobias Nipkow
2019	J	`jnl`	Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra. Arch. Formal Proofs Peter Lammich, Tobias Nipkow
2019	B	`conf`	Trustworthy Graph Algorithms (Invited Talk). MFCS Mohammad Abdulaziz, Kurt Mehlhorn, Tobias Nipkow
2019	J	`jnl`	Trustworthy Graph Algorithms. CoRR Mohammad Abdulaziz, Kurt Mehlhorn, Tobias Nipkow
2018	A	`conf`	A Verified Compiler from Isabelle/HOL to CakeML. ESOP Lars Hupel, Tobias Nipkow
2018	—	`conf`	Hoare Logics for Time Bounds - A Study in Meta Theory. TACAS (1) Maximilian P. L. Haslbeck, Tobias Nipkow
2018	J	`jnl`	Hoare Logics for Time Bounds. Arch. Formal Proofs Maximilian P. L. Haslbeck, Tobias Nipkow
2018	J	`jnl`	Monadification, Memoization and Dynamic Programming. Arch. Formal Proofs Simon Wimmer, Shuwei Hu, Tobias Nipkow
2018	J	`jnl`	Optimal Binary Search Trees. Arch. Formal Proofs Tobias Nipkow, Dániel Somogyi
2018	J	`jnl`	Treaps. Arch. Formal Proofs Max W. Haslbeck, Manuel Eberl, Tobias Nipkow
2018	B	`conf`	Verified Analysis of Random Binary Tree Structures. ITP Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
2018	B	`conf`	Verified Memoization and Dynamic Programming. ITP Simon Wimmer, Shuwei Hu, Tobias Nipkow
2018	J	`jnl`	Weight-Balanced Trees. Arch. Formal Proofs Tobias Nipkow, Stefan Dirix
2017	J	`jnl`	A Verified Compiler for Probability Density Functions. CoRR Manuel Eberl, Johannes Hölzl, Tobias Nipkow
2017	B	`conf`	Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL. IFM Albert Rizaldi, Jonas Keinholz, Monika Huber, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf, Tobias Nipkow
2017	—	`conf`	Formalized Proof Systems for Propositional Logic. TYPES Julius Michaelis, Tobias Nipkow
2017	J	`jnl`	Propositional Proof Systems. Arch. Formal Proofs Julius Michaelis, Tobias Nipkow
2017	J	`jnl`	Root-Balanced Tree. Arch. Formal Proofs Tobias Nipkow
2017	—	`ch.`	Software-Verifikation. 50 Jahre Universitäts-Informatik in München Dirk Beyer, Rolf Hennicker, Martin Hofmann, Tobias Nipkow, Martin Wirsing
2017	B	`conf`	Verified Root-Balanced Trees. APLAS Tobias Nipkow
2016	J	`jnl`	Abstract Interpretation of Annotated Commands. Arch. Formal Proofs Tobias Nipkow
2016	J	`jnl`	Analysis of List Update Algorithms. Arch. Formal Proofs Maximilian P. L. Haslbeck, Tobias Nipkow
2016	B	`conf`	Automatic Functional Correctness Proofs for Functional Search Trees. ITP Tobias Nipkow
2016	J	`jnl`	Pairing Heap. Arch. Formal Proofs Hauke Brinkop, Tobias Nipkow
2016	B	`conf`	Verified Analysis of Functional Data Structures. FSCD Tobias Nipkow
2016	—	`conf`	Verified Analysis of List Update Algorithms. FSTTCS Maximilian P. L. Haslbeck, Tobias Nipkow
2015	A	`conf`	A Verified Compiler for Probability Density Functions. ESOP Manuel Eberl, Johannes Hölzl, Tobias Nipkow
2015	J	`jnl`	A formal proof of the Kepler conjecture. CoRR Thomas C. 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 M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller
2015	B	`conf`	Amortized Complexity Verified. ITP Tobias Nipkow
2015	C	`conf`	Mining the Archive of Formal Proofs. CICM Jasmin Christian Blanchette, Max W. Haslbeck, Daniel Matichuk, Tobias Nipkow
2015	J	`jnl`	Parameterized Dynamic Tables. Arch. Formal Proofs Tobias Nipkow
2015	J	`jnl`	Trie. Arch. Formal Proofs Andreas Lochbihler, Tobias Nipkow
2015	J	`jnl`	Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. Dmitriy Traytel, Tobias Nipkow
2014	J	`jnl`	A Fully Verified Executable LTL Model Checker. Arch. Formal Proofs Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
2014	J	`jnl`	A Verified Compiler for Probability Density Functions. Arch. Formal Proofs Manuel Eberl, Johannes Hölzl, Tobias Nipkow
2014	J	`jnl`	Amortized Complexity Verified. Arch. Formal Proofs Tobias Nipkow
2014	—	`ch.`	Applications of Interactive Proof to Data Flow Analysis and Security. Software Systems Safety Gerwin Klein, Tobias Nipkow
2014	J	`jnl`	Boolean Expression Checkers. Arch. Formal Proofs Tobias Nipkow
2014	—	`book`	Concrete Semantics - With Isabelle/HOL Tobias Nipkow, Gerwin Klein
2014	J	`jnl`	Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions. Arch. Formal Proofs Dmitriy Traytel, Tobias Nipkow
2014	C	`conf`	Experience report: the next 1100 Haskell programmers. Haskell Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel
2014	J	`jnl`	Making security type systems less ad hoc. it Inf. Technol. Tobias Nipkow, Andrei Popescu
2014	J	`jnl`	Priority Queues Based on Braun Trees. Arch. Formal Proofs Tobias Nipkow
2014	J	`jnl`	Skew Heap. Arch. Formal Proofs Tobias Nipkow
2014	J	`jnl`	Splay Tree. Arch. Formal Proofs Tobias Nipkow
2014	B	`conf`	Unified Decision Procedures for Regular Expression Equivalence. ITP Tobias Nipkow, Dmitriy Traytel
2014	J	`jnl`	Unified Decision Procedures for Regular Expression Equivalence. Arch. Formal Proofs Tobias Nipkow, Dmitriy Traytel
2013	B	`conf`	A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions. TABLEAUX Tobias Nipkow, Maximilian P. L. Haslbeck
2013	A*	`conf`	A Fully Verified Executable LTL Model Checker. CAV Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
2013	B	`conf`	Data Refinement in Isabelle/HOL. ITP Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow
2013	J	`jnl`	Deduction and Arithmetic (Dagstuhl Seminar 13411). Dagstuhl Reports Nikolaj S. Bjørner, Reiner Hähnle, Tobias Nipkow, Christoph Weidenbach
2013	J	`jnl`	Formal Verification of Language-Based Concurrent Noninterference. J. Formaliz. Reason. Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2013	B	`conf`	Formalizing Probabilistic Noninterference. CPP Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2013	B	`conf`	Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. CALCO Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2013	A	`conf`	Verified decision procedures for MSO on words based on derivatives of regular expressions. ICFP Dmitriy Traytel, Tobias Nipkow
2012	J	`jnl`	A compiled implementation of normalisation by evaluation. J. Funct. Program. Klaus Aehlig, Florian Haftmann, Tobias Nipkow
2012	B	`conf`	Abstract Interpretation of Annotated Commands. ITP Tobias Nipkow
2012	—	`ch.`	Interactive Proof: Introduction to Isabelle/HOL. Software Safety and Security Tobias Nipkow
2012	—	`conf`	Interactive verification of Markov chains: Two distributed protocol case studies QFM Johannes Hölzl, Tobias Nipkow
2012	J	`jnl`	Markov Models. Arch. Formal Proofs Johannes Hölzl, Tobias Nipkow
2012	J	`jnl`	Proof Pearl: Regular Expression Equivalence and Relation Algebra. J. Autom. Reason. Alexander Krauss, Tobias Nipkow
2012	B	`conf`	Proving Concurrent Noninterference. CPP Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2012	—	`book`	Software Safety and Security - Tools for Analysis and Verification Software Safety and Security Tobias Nipkow, Orna Grumberg, Benedikt Hauptmann
2012	B	`conf`	Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs. VMCAI Tobias Nipkow
2012	A	`conf`	Verifying pCTL Model Checking. TACAS Johannes Hölzl, Tobias Nipkow
2011	—	`conf`	Automatic Proof and Disproof in Isabelle/HOL. FroCoS Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow
2011	B	`conf`	Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. APLAS Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow
2011	J	`jnl`	Gauss-Jordan Elimination for Matrices Represented as Functions. Arch. Formal Proofs Tobias Nipkow
2011	J	`jnl`	Majority Vote Algorithm Revisited Again. Int. J. Softw. Informatics Tobias Nipkow
2011	B	`conf`	Proof Pearl: The Marriage Theorem. CPP Dongchen Jiang, Tobias Nipkow
2011	B	`conf`	Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. ITP Tobias Nipkow
2010	J	`jnl`	A Revision of the Proof of the Kepler Conjecture. Discret. Comput. Geom. Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller
2010	Misc	`conf`	Code Generation via Higher-Order Rewrite Systems. FLOPS Florian Haftmann, Tobias Nipkow
2010	J	`jnl`	Deduktion: von der Theorie zur Anwendung. Inform. Spektrum Franz Baader, Bernhard Beckert, Tobias Nipkow
2010	J	`jnl`	Hall's Marriage Theorem. Arch. Formal Proofs Dongchen Jiang, Tobias Nipkow
2010	J	`jnl`	Linear Quantifier Elimination. J. Autom. Reason. Tobias Nipkow
2010	J	`jnl`	List Index. Arch. Formal Proofs Tobias Nipkow
2010	B	`conf`	Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. ITP Jasmin Christian Blanchette, Tobias Nipkow
2010	J	`jnl`	Regular Sets and Expressions. Arch. Formal Proofs Alexander Krauss, Tobias Nipkow
2010	A	`conf`	Sledgehammer: Judgement Day. IJCAR Sascha Böhme, Tobias Nipkow
2009	—	`conf`	09411 Abstracts Collection - Interaction versus Automation: The two Faces of Deduction. Interaction versus Automation: The two Faces of Deduction Thomas Ball, Jürgen Giesl, Reiner Hähnle, Tobias Nipkow
2009	—	`conf`	09411 Executive Summary - Interaction versus Automation: The two Faces of Deductions. Interaction versus Automation: The two Faces of Deduction Thomas Ball, Jürgen Giesl, Reiner Hähnle, Tobias Nipkow
2009	J	`jnl`	Flyspeck II: the basic linear programs. Ann. Math. Artif. Intell. Steven Obua, Tobias Nipkow
2009	—	`ed.`	Interaction versus Automation: The two Faces of Deduction, 04.10. - 09.10.2009 Interaction versus Automation: The two Faces of Deduction Thomas Ball, Jürgen Giesl, Reiner Hähnle, Tobias Nipkow
2009	J	`jnl`	Social Choice Theory in HOL. J. Autom. Reason. Tobias Nipkow
2009	—	`ed.`	Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings TPHOLs Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel
2008	—	`conf`	A Compiled Implementation of Normalization by Evaluation. TPHOLs Klaus Aehlig, Florian Haftmann, Tobias Nipkow
2008	J	`jnl`	Arrow and Gibbard-Satterthwaite. Arch. Formal Proofs Tobias Nipkow
2008	J	`jnl`	Fun With Functions. Arch. Formal Proofs Tobias Nipkow
2008	J	`jnl`	Fun With Tilings. Arch. Formal Proofs Tobias Nipkow, Lawrence C. Paulson
2008	A	`conf`	Linear Quantifier Elimination. IJCAR Tobias Nipkow
2008	J	`jnl`	Normalization by Evaluation. Arch. Formal Proofs Klaus Aehlig, Tobias Nipkow
2008	J	`jnl`	Preface. J. Autom. Reason. Serge Autexier, Heiko Mantel, Stephan Merz, Tobias Nipkow
2008	J	`jnl`	Proof Synthesis and Reflection for Linear Arithmetic. J. Autom. Reason. Amine Chaieb, Tobias Nipkow
2008	J	`jnl`	Quantifier Elimination for Linear Arithmetic. Arch. Formal Proofs Tobias Nipkow
2008	—	`conf`	The Isabelle Framework. TPHOLs Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow
2007	C	`conf`	C++ ist typsicher? Garantiert! Software Engineering Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip
2007	—	`conf`	Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. TPHOLs Lukas Bulwahn, Alexander Krauss, Tobias Nipkow
2007	—	`ed.`	Proceedings of the 6th International Workshop on Automated Verification of Critical Systems, AVoCS 2006, Nancy, France, September 18-19, 2006 AVoCS Stephan Merz, Tobias Nipkow
2007	—	`conf`	Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic. VERIFY Tobias Nipkow
2006	J	`jnl`	A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. Gerwin Klein, Tobias Nipkow
2006	J	`jnl`	Abstract Hoare Logics. Arch. Formal Proofs Tobias Nipkow
2006	A	`conf`	An operational semantics and type safety prooffor multiple inheritance in C++. OOPSLA Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip
2006	B	`ed.`	FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings FM Jayadev Misra, Tobias Nipkow, Emil Sekerinski
2006	A	`conf`	Flyspeck I: Tame Graphs. IJCAR Tobias Nipkow, Gertrud Bauer, Paula Schultz
2006	J	`jnl`	Flyspeck I: Tame Graphs. Arch. Formal Proofs Gertrud Bauer, Tobias Nipkow
2006	J	`jnl`	Hotel Key Card System. Arch. Formal Proofs Tobias Nipkow
2006	—	`conf`	Preface. AVoCS Stephan Merz, Tobias Nipkow
2006	C	`conf`	Verifying a Hotel Key Card System. ICTAC Tobias Nipkow
2005	A	`conf`	Asserting Bytecode Safety. ESOP Martin Wildmoser, Tobias Nipkow
2005	—	`conf`	Bytecode Analysis for Proof Carrying Code. Bytecode@ETAPS Martin Wildmoser, Amine Chaieb, Tobias Nipkow
2005	J	`jnl`	Jinja is not Java. Arch. Formal Proofs Gerwin Klein, Tobias Nipkow
2005	—	`conf`	Proof Pearl: Defining Functions over Finite Sets. TPHOLs Tobias Nipkow, Lawrence C. Paulson
2005	J	`jnl`	Proving pointer programs in higher-order logic. Inf. Comput. Farhad Mehta, Tobias Nipkow
2005	—	`conf`	Towards a Verified Enumeration of All Tame Plane Graphs. Mathematics, Algorithms, Proofs Tobias Nipkow, Gertrud Bauer
2005	B	`conf`	Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. LPAR Amine Chaieb, Tobias Nipkow
2004	J	`jnl`	AVL Trees. Arch. Formal Proofs Tobias Nipkow, Cornelia Pusch
2004	—	`conf`	Certifying Machine Code Safety: Shallow Versus Deep Embedding. TPHOLs Martin Wildmoser, Tobias Nipkow
2004	J	`jnl`	Compiling Exceptions Correctly. Arch. Formal Proofs Tobias Nipkow
2004	J	`jnl`	Functional Automata. Arch. Formal Proofs Tobias Nipkow
2004	J	`jnl`	Mini ML. Arch. Formal Proofs Wolfgang Naraschewski, Tobias Nipkow
2004	—	`conf`	Prototyping Proof Carrying Code. IFIP TCS Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz
2004	B	`conf`	Random Testing in Isabelle/HOL. SEFM Stefan Berghofer, Tobias Nipkow
2003	J	`jnl`	Java Bytecode Verification. J. Autom. Reason. Tobias Nipkow
2003	A	`conf`	Proving Pointer Programs in Higher-Order Logic. CADE Farhad Mehta, Tobias Nipkow
2003	J	`jnl`	Verified bytecode verifiers. Theor. Comput. Sci. Gerwin Klein, Tobias Nipkow
2002	—	`conf`	Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. FME David von Oheimb, Tobias Nipkow
2002	B	`conf`	Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. CSL Tobias Nipkow
2002	—	`book`	Isabelle/HOL - A Proof Assistant for Higher-Order Logic Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel
2002	—	`conf`	Structured Proofs in Isar/HOL. TYPES Tobias Nipkow
2002	—	`conf`	The 5 Colour Theorem in Isabelle/Isar. TPHOLs Gertrud Bauer, Tobias Nipkow
2001	A	`ed.`	Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings IJCAR Rajeev Goré, Alexander Leitsch, Tobias Nipkow
2001	J	`jnl`	More Church-Rosser Proofs. J. Autom. Reason. Tobias Nipkow
2001	B	`conf`	Verified Bytecode Verifiers. FoSSaCS Tobias Nipkow
2001	J	`jnl`	Verified lightweight bytecode verification. Concurr. Comput. Pract. Exp. Gerwin Klein, Tobias Nipkow
2000	—	`conf`	Executing Higher Order Logic. TYPES Stefan Berghofer, Tobias Nipkow
2000	J	`jnl`	Preface. Inf. Comput. Tobias Nipkow
2000	—	`conf`	Proof Terms for Simply Typed Higher Order Logic. TPHOLs Stefan Berghofer, Tobias Nipkow
2000	—	`conf`	Workshop über Rigorose Entwicklung software-intensiver Systeme. GI Jahrestagung Martin Wirsing, Martin Gogolla, Hans-Jörg Kreowski, Tobias Nipkow, Wolfgang Reif
1999	J	`jnl`	HOLCF=HOL+LCF. J. Funct. Program. Olaf Müller, Tobias Nipkow, David von Oheimb, Oscar Slotosch
1999	A	`conf`	Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract). CADE Tobias Nipkow
1999	—	`conf`	Machine-Checking the Java Specification: Proving Type-Safety. Formal Syntax and Semantics of Java David von Oheimb, Tobias Nipkow
1999	B	`conf`	Owicki/Gries in Isabelle/HOL. FASE Tobias Nipkow, Leonor Prensa Nieto
1999	J	`jnl`	Type Inference Verified: Algorithm W in Isabelle/HOL. J. Autom. Reason. Wolfgang Naraschewski, Tobias Nipkow
1998	J	`jnl`	Higher-Order Rewrite Systems and Their Confluence. Theor. Comput. Sci. Richard Mayr, Tobias Nipkow
1998	A*	`conf`	Java POPL Tobias Nipkow, David von Oheimb
1998	—	`ed.`	Rewriting Techniques and Applications, 9th International Conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998, Proceedings RTA Tobias Nipkow
1998	—	`book`	Term rewriting and all that. Franz Baader, Tobias Nipkow
1998	—	`conf`	Verified Lexical Analysis. TPHOLs Tobias Nipkow
1998	J	`jnl`	Winskel is (almost) Right: Towards a Mechanized Semantics. Formal Aspects Comput. Tobias Nipkow
1997	—	`conf`	Traces of I/O-Automata in Isabelle/HOLCF. TAPSOFT Olaf Müller, Tobias Nipkow
1996	—	`conf`	Formal Verification of Algorithm W: The Monomorphic Case. TPHOLs Dieter Nazareth, Tobias Nipkow
1996	A	`conf`	More Church-Rosser Proofs (in Isabelle/HOL). CADE Tobias Nipkow
1996	—	`conf`	Type Inference Verified: Algorithm W in Isabelle/HOL. TYPES Wolfgang Naraschewski, Tobias Nipkow
1996	—	`conf`	Winskel is (Almost) Right: Towards a Mechanized Semantics Textbook. FSTTCS Tobias Nipkow
1995	A	`conf`	Combining Model Checking and Deduction for I/O-Automata. TACAS Olaf Müller, Tobias Nipkow
1995	—	`conf`	Higher-Order Rewrite Systems (Abstract). RTA Tobias Nipkow
1995	J	`jnl`	Type Reconstruction for Type Classes. J. Funct. Program. Tobias Nipkow, Christian Prehofer
1994	—	`ed.`	Higher-Order Algebra, Logic, and Term Rewriting, First International Workshop, HOA '93, Amsterdam, The Netherlands, September 23-24, 1993, Selected Papers HOA Jan Heering, Karl Meinke, Bernhard Möller, Tobias Nipkow
1994	—	`conf`	I/Q Automata in Isabelle/HOL. TYPES Tobias Nipkow, Konrad Slind
1994	—	`conf`	Interpreter Verification for a Functional Language. FSTTCS Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, Birgit Schieder
1994	J	`jnl`	Reduction and Unification in Lambda Calculi with a General Notion of Subtype. J. Autom. Reason. Zhenyu Qian, Tobias Nipkow
1994	—	`ed.`	Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers TYPES Henk Barendregt, Tobias Nipkow
1993	A*	`conf`	Functional Unification of Higher-Order Patterns LICS Tobias Nipkow
1993	—	`conf`	Orthogonal Higher-Order Rewrite Systems are Confluent. TLCA Tobias Nipkow
1993	A*	`conf`	Type Checking Type Classes. POPL Tobias Nipkow, Christian Prehofer
1992	A	`conf`	Isabelle-91. CADE Tobias Nipkow, Lawrence C. Paulson
1992	A	`conf`	Reduction and Unification in Lambda Calculi with Subtypes. CADE Tobias Nipkow, Zhenyu Qian
1991	J	`jnl`	Combining Matching Algorithms: The Regular Case. J. Symb. Comput. Tobias Nipkow
1991	J	`jnl`	Constructive Rewriting. Comput. J. Tobias Nipkow
1991	A*	`conf`	Higher-Order Critical Pairs LICS Tobias Nipkow
1991	—	`conf`	Modular Higher-Order RTA Tobias Nipkow, Zhenyu Qian
1991	—	`conf`	Type Classes and Overloading Resolution via Order-Sorted Unification. FPCA Tobias Nipkow, Gregor Snelting
1990	—	`conf`	Automating Squiggol. Programming Concepts and Methods Ursula Martin, Tobias Nipkow
1990	—	`conf`	Higher-Order Unification, Polymorphism, and Subsorts (Extended Abstract). CTRS Tobias Nipkow
1990	A	`conf`	Ordered Rewriting and Confluence. CADE Ursula Martin, Tobias Nipkow
1990	A*	`conf`	Proof Transformations for Equational Theories LICS Tobias Nipkow
1990	J	`jnl`	Unification in Primal Algebras, Their Powers and Their Varieties J. ACM Tobias Nipkow
1989	J	`jnl`	Boolean Unification - The Story So Far. J. Symb. Comput. Ursula Martin, Tobias Nipkow
1989	—	`conf`	Combining Matching Algorithms: The Rectangular Case. RTA Tobias Nipkow
1989	J	`jnl`	Equational Reasoning in Isabelle. Sci. Comput. Program. Tobias Nipkow
1989	—	`conf`	Formal Verification of Data Type Refinement - Theory and Practice. REX Workshop Tobias Nipkow
1989	J	`jnl`	Term Rewriting and Beyond - Theorem Proving in Isabelle. Formal Aspects Comput. Tobias Nipkow
1988	J	`jnl`	Unification in Boolean Rings. J. Autom. Reason. Ursula Martin, Tobias Nipkow
1988	—	`conf`	Unification in Primal Algebras. CAAP Tobias Nipkow
1987	A	`conf`	Are Homomorphisms Sufficient for Behavioural Implementations of Deterministic and Nondeterministic Data Types? STACS Tobias Nipkow
1987	—	`conf`	Observing Non-Deterministic Data Types. ADT Tobias Nipkow
1986	—	`conf`	Behavioural Implementations of Non-Deterministic Data Types. ADT Tobias Nipkow
1986	—	`—`	Behavioural implementation concepts for nondeterministic data types. Tobias Nipkow
1986	J	`jnl`	Non-deterministic Data Types: Models and Implementations. Acta Informatica Tobias Nipkow
1986	A	`conf`	Unification in Boolean Rings. CADE Ursula Martin, Tobias Nipkow
1983	—	`conf`	A decidability result about sufficient-completeness of axiomatically specified abstract data types. Theoretical Computer Science Tobias Nipkow, Gerhard Weikum