Tobias Nipkow

ORCID

Publication Activity (10 Years)

Years Active: 1983-2024
Publications (10 Years): 56

Top Venues

University of Manchester, UK (PHD)

Education History

University of Manchester, UK

PHD

Publications

Tobias Nipkow
Gale-Shapley Verified. J. Autom. Reason. 68 (2) (2024)
Tobias Nipkow
Alpha-Beta Pruning. Arch. Formal Proofs 2024 (2024)
Tobias Nipkow
Region Quadtrees Verified. Taming the Infinities of Concurrency (2024)
Tobias Nipkow
Region Quadtrees. Arch. Formal Proofs 2024 (2024)
Balázs Tóth, Tobias Nipkow
Real-Time Double-Ended Queue Verified (Proof Pearl). ITP (2023)
Katharina Kreuzer, Tobias Nipkow
Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. CADE (2023)
Katharina Kreuzer, Tobias Nipkow
Verification of NP-hardness Reduction Functions for Exact Lattice Problems. CoRR (2023)
Simon Roßkopf, Tobias Nipkow
A Formalization and Proof Checker for Isabelle's Metalogic. J. Autom. Reason. 67 (1) (2023)
Robin Eßmann, Tobias Nipkow, Simon Robillard, Ujkan Sulejmani
Verified Approximation Algorithms. Log. Methods Comput. Sci. 18 (1) (2022)
Niels Mündler, Tobias Nipkow
A Verified Implementation of B+-Trees in Isabelle/HOL. CoRR (2022)
Balázs Tóth, Tobias Nipkow
Real-Time Double-Ended Queue. Arch. Formal Proofs 2022 (2022)
Niels Mündler, Tobias Nipkow
-Trees in Isabelle/HOL. ICTAC (2022)
Tobias Nipkow, Simon Roßkopf
Isabelle's Metalogic: Formalization and Proof Checker. CoRR (2021)
Tobias Nipkow, Simon Roßkopf
Isabelle's Metalogic: Formalization and Proof Checker. Arch. Formal Proofs 2021 (2021)
Robin Eßmann, Tobias Nipkow, Simon Robillard
Verified Approximation Algorithms. CoRR (2021)
Tobias Nipkow
Gale-Shapley Algorithm. Arch. Formal Proofs 2021 (2021)
Tobias Nipkow, Simon Roßkopf
Isabelle's Metalogic: Formalization and Proof Checker. CADE (2021)
Lukas Stevens, Tobias Nipkow
A Verified Decision Procedure for Orders in Isabelle/HOL. CoRR (2021)
Lukas Stevens, Tobias Nipkow
A Verified Decision Procedure for Orders in Isabelle/HOL. ATVA (2021)
Tobias Nipkow
Teaching algorithms and data structures with a proof assistant (invited talk). CPP (2021)
Tobias Nipkow, Manuel Eberl, Maximilian P. L. Haslbeck
Verified Textbook Algorithms - A Biased Survey. ATVA (2020)
Tobias Nipkow, Thomas Sewell
Proof pearl: Braun trees. CPP (2020)
Robin Eßmann, Tobias Nipkow, Simon Robillard
Verified Approximation Algorithms. IJCAR (2) (2020)
Robin Eßmann, Tobias Nipkow, Simon Robillard
Verified Approximation Algorithms. Arch. Formal Proofs 2020 (2020)
Martin Rau, Tobias Nipkow
Verification of Closest Pair of Points Algorithms. IJCAR (2) (2020)
Martin Rau, Tobias Nipkow
Closest Pair of Points Algorithms. Arch. Formal Proofs 2020 (2020)
Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
Verified Analysis of Random Binary Tree Structures. J. Autom. Reason. 64 (5) (2020)
Tobias Nipkow, Hauke Brinkop
Amortized Complexity Verified. J. Autom. Reason. 62 (3) (2019)
Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel
From LCF to Isabelle/HOL. CoRR (2019)
Peter Lammich, Tobias Nipkow
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra. Arch. Formal Proofs 2019 (2019)
Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel
From LCF to Isabelle/HOL. Formal Aspects Comput. 31 (6) (2019)
Mohammad Abdulaziz, Kurt Mehlhorn, Tobias Nipkow
Trustworthy Graph Algorithms. CoRR (2019)
Peter Lammich, Tobias Nipkow
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. ITP (2019)
Mohammad Abdulaziz, Kurt Mehlhorn, Tobias Nipkow
Trustworthy Graph Algorithms (Invited Talk). MFCS (2019)
Peter Lammich, Tobias Nipkow
Priority Search Trees. Arch. Formal Proofs 2019 (2019)
Maximilian P. L. Haslbeck, Tobias Nipkow
Hoare Logics for Time Bounds - A Study in Meta Theory. TACAS (1) (2018)
Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
Verified Analysis of Random Binary Tree Structures. ITP (2018)
Simon Wimmer, Shuwei Hu, Tobias Nipkow
Verified Memoization and Dynamic Programming. ITP (2018)
Tobias Nipkow, Dániel Somogyi
Optimal Binary Search Trees. Arch. Formal Proofs 2018 (2018)
Lars Hupel, Tobias Nipkow
A Verified Compiler from Isabelle/HOL to CakeML. ESOP (2018)
Tobias Nipkow, Stefan Dirix
Weight-Balanced Trees. Arch. Formal Proofs 2018 (2018)
Max W. Haslbeck, Manuel Eberl, Tobias Nipkow
Treaps. Arch. Formal Proofs 2018 (2018)
Maximilian P. L. Haslbeck, Tobias Nipkow
Hoare Logics for Time Bounds. Arch. Formal Proofs 2018 (2018)
Simon Wimmer, Shuwei Hu, Tobias Nipkow
Monadification, Memoization and Dynamic Programming. Arch. Formal Proofs 2018 (2018)
Julius Michaelis, Tobias Nipkow
Formalized Proof Systems for Propositional Logic. TYPES (2017)
Manuel Eberl, Johannes Hölzl, Tobias Nipkow
A Verified Compiler for Probability Density Functions. CoRR (2017)
Tobias Nipkow
Verified Root-Balanced Trees. APLAS (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. IFM (2017)
Tobias Nipkow
Root-Balanced Tree. Arch. Formal Proofs 2017 (2017)
Julius Michaelis, Tobias Nipkow
Propositional Proof Systems. Arch. Formal Proofs 2017 (2017)
Maximilian P. L. Haslbeck, Tobias Nipkow
Analysis of List Update Algorithms. Arch. Formal Proofs 2016 (2016)
Tobias Nipkow
Abstract Interpretation of Annotated Commands. Arch. Formal Proofs 2016 (2016)
Tobias Nipkow
Automatic Functional Correctness Proofs for Functional Search Trees. ITP (2016)
Hauke Brinkop, Tobias Nipkow
Pairing Heap. Arch. Formal Proofs 2016 (2016)
Tobias Nipkow
Verified Analysis of Functional Data Structures. FSCD (2016)
Maximilian P. L. Haslbeck, Tobias Nipkow
Verified Analysis of List Update Algorithms. FSTTCS (2016)
Dmitriy Traytel, Tobias Nipkow
Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. 25 (2015)
Jasmin Christian Blanchette, Max W. Haslbeck, Daniel Matichuk, Tobias Nipkow
Mining the Archive of Formal Proofs. CICM (2015)
Tobias Nipkow
Amortized Complexity Verified. ITP (2015)
Andreas Lochbihler, Tobias Nipkow
Trie. Arch. Formal Proofs 2015 (2015)
Tobias Nipkow
Parameterized Dynamic Tables. Arch. Formal Proofs 2015 (2015)
Manuel Eberl, Johannes Hölzl, Tobias Nipkow
A Verified Compiler for Probability Density Functions. ESOP (2015)
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
A formal proof of the Kepler conjecture. CoRR (2015)
Tobias Nipkow
Boolean Expression Checkers. Arch. Formal Proofs 2014 (2014)
Tobias Nipkow
Skew Heap. Arch. Formal Proofs 2014 (2014)
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
A Fully Verified Executable LTL Model Checker. Arch. Formal Proofs 2014 (2014)
Tobias Nipkow
Priority Queues Based on Braun Trees. Arch. Formal Proofs 2014 (2014)
Tobias Nipkow, Dmitriy Traytel
Unified Decision Procedures for Regular Expression Equivalence. ITP (2014)
Tobias Nipkow
Amortized Complexity Verified. Arch. Formal Proofs 2014 (2014)
Tobias Nipkow, Dmitriy Traytel
Unified Decision Procedures for Regular Expression Equivalence. Arch. Formal Proofs 2014 (2014)
Tobias Nipkow, Andrei Popescu
Making security type systems less ad hoc. it Inf. Technol. 56 (6) (2014)
Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel
Experience report: the next 1100 Haskell programmers. Haskell (2014)
Tobias Nipkow
Splay Tree. Arch. Formal Proofs 2014 (2014)
Dmitriy Traytel, Tobias Nipkow
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions. Arch. Formal Proofs 2014 (2014)
Manuel Eberl, Johannes Hölzl, Tobias Nipkow
A Verified Compiler for Probability Density Functions. Arch. Formal Proofs 2014 (2014)
Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow
Data Refinement in Isabelle/HOL. ITP (2013)
Nikolaj Bjørner, Reiner Hähnle, Tobias Nipkow, Christoph Weidenbach
Deduction and Arithmetic (Dagstuhl Seminar 13411). Dagstuhl Reports 3 (10) (2013)
Tobias Nipkow, Maximilian P. L. Haslbeck
A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions. TABLEAUX (2013)
Dmitriy Traytel, Tobias Nipkow
Verified decision procedures for MSO on words based on derivatives of regular expressions. ICFP (2013)
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Formal Verification of Language-Based Concurrent Noninterference. J. Formaliz. Reason. 6 (1) (2013)
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
A Fully Verified Executable LTL Model Checker. CAV (2013)
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Formalizing Probabilistic Noninterference. CPP (2013)
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. CALCO (2013)
Johannes Hölzl, Tobias Nipkow
Interactive verification of Markov chains: Two distributed protocol case studies QFM (2012)
Tobias Nipkow
Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs. VMCAI (2012)
Klaus Aehlig, Florian Haftmann, Tobias Nipkow
A compiled implementation of normalisation by evaluation. J. Funct. Program. 22 (1) (2012)
Johannes Hölzl, Tobias Nipkow
Markov Models. Arch. Formal Proofs 2012 (2012)
Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Proving Concurrent Noninterference. CPP (2012)
Alexander Krauss, Tobias Nipkow
Proof Pearl: Regular Expression Equivalence and Relation Algebra. J. Autom. Reason. 49 (1) (2012)
Johannes Hölzl, Tobias Nipkow
Verifying pCTL Model Checking. TACAS (2012)
Tobias Nipkow
Abstract Interpretation of Annotated Commands. ITP (2012)
Tobias Nipkow
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. ITP (2011)
Tobias Nipkow
Majority Vote Algorithm Revisited Again. Int. J. Softw. Informatics 5 (1-2) (2011)
Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. APLAS (2011)
Tobias Nipkow
Gauss-Jordan Elimination for Matrices Represented as Functions. Arch. Formal Proofs 2011 (2011)
Dongchen Jiang, Tobias Nipkow
Proof Pearl: The Marriage Theorem. CPP (2011)
Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow
Automatic Proof and Disproof in Isabelle/HOL. FroCoS (2011)
Franz Baader, Bernhard Beckert, Tobias Nipkow
Deduktion: von der Theorie zur Anwendung. Inform. Spektrum 33 (5) (2010)
Florian Haftmann, Tobias Nipkow
Code Generation via Higher-Order Rewrite Systems. FLOPS (2010)
Alexander Krauss, Tobias Nipkow
Regular Sets and Expressions. Arch. Formal Proofs 2010 (2010)

Tobias Nipkow.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Tobias Nipkow