![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Tobias Nipkow
Person information
- affiliation: Technical University Munich, Germany
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j88]Tobias Nipkow:
Region Quadtrees. Arch. Formal Proofs 2024 (2024) - [j87]Tobias Nipkow:
Alpha-Beta Pruning. Arch. Formal Proofs 2024 (2024) - [j86]Tobias Nipkow
:
Gale-Shapley Verified. J. Autom. Reason. 68(2): 12 (2024) - [c106]Tobias Nipkow:
Region Quadtrees Verified. Taming the Infinities of Concurrency 2024: 243-254 - 2023
- [j85]Simon Roßkopf
, Tobias Nipkow
:
A Formalization and Proof Checker for Isabelle's Metalogic. J. Autom. Reason. 67(1): 1 (2023) - [c105]Katharina Kreuzer
, Tobias Nipkow
:
Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. CADE 2023: 365-381 - [c104]Balázs Tóth, Tobias Nipkow:
Real-Time Double-Ended Queue Verified (Proof Pearl). ITP 2023: 29:1-29:18 - [i13]Katharina Kreuzer, Tobias Nipkow:
Verification of NP-hardness Reduction Functions for Exact Lattice Problems. CoRR abs/2306.08375 (2023) - 2022
- [j84]Balázs Tóth, Tobias Nipkow:
Real-Time Double-Ended Queue. Arch. Formal Proofs 2022 (2022) - [j83]Robin Eßmann, Tobias Nipkow, Simon Robillard, Ujkan Sulejmani:
Verified Approximation Algorithms. Log. Methods Comput. Sci. 18(1) (2022) - [c103]Niels Mündler
, Tobias Nipkow
:
A Verified Implementation of B+-Trees in Isabelle/HOL. ICTAC 2022: 324-341 - [i12]Niels Mündler, Tobias Nipkow:
A Verified Implementation of B+-Trees in Isabelle/HOL. CoRR abs/2208.09066 (2022) - 2021
- [j82]Tobias Nipkow:
Gale-Shapley Algorithm. Arch. Formal Proofs 2021 (2021) - [j81]Tobias Nipkow, Simon Roßkopf:
Isabelle's Metalogic: Formalization and Proof Checker. Arch. Formal Proofs 2021 (2021) - [c102]Lukas Stevens
, Tobias Nipkow
:
A Verified Decision Procedure for Orders in Isabelle/HOL. ATVA 2021: 127-143 - [c101]Tobias Nipkow
, Simon Roßkopf
:
Isabelle's Metalogic: Formalization and Proof Checker. CADE 2021: 93-110 - [c100]Tobias Nipkow
:
Teaching algorithms and data structures with a proof assistant (invited talk). CPP 2021: 1-3 - [i11]Tobias Nipkow, Simon Roßkopf:
Isabelle's Metalogic: Formalization and Proof Checker. CoRR abs/2104.12224 (2021) - [i10]Lukas Stevens, Tobias Nipkow:
A Verified Decision Procedure for Orders in Isabelle/HOL. CoRR abs/2104.13117 (2021) - [i9]Robin Eßmann, Tobias Nipkow, Simon Robillard:
Verified Approximation Algorithms. CoRR abs/2104.13851 (2021) - 2020
- [j80]Robin Eßmann, Tobias Nipkow, Simon Robillard:
Verified Approximation Algorithms. Arch. Formal Proofs 2020 (2020) - [j79]Martin Rau, Tobias Nipkow:
Closest Pair of Points Algorithms. Arch. Formal Proofs 2020 (2020) - [j78]Manuel Eberl
, Max W. Haslbeck
, Tobias Nipkow
:
Verified Analysis of Random Binary Tree Structures. J. Autom. Reason. 64(5): 879-910 (2020) - [c99]Tobias Nipkow
, Manuel Eberl
, Maximilian P. L. Haslbeck
:
Verified Textbook Algorithms - A Biased Survey. ATVA 2020: 25-53 - [c98]Robin Eßmann
, Tobias Nipkow
, Simon Robillard
:
Verified Approximation Algorithms. IJCAR (2) 2020: 291-306 - [c97]Martin Rau
, Tobias Nipkow
:
Verification of Closest Pair of Points Algorithms. IJCAR (2) 2020: 341-357 - [c96]Tobias Nipkow, Thomas Sewell:
Proof pearl: Braun trees. CPP 2020: 18-31
2010 – 2019
- 2019
- [j77]Peter Lammich, Tobias Nipkow:
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra. Arch. Formal Proofs 2019 (2019) - [j76]Peter Lammich, Tobias Nipkow:
Priority Search Trees. Arch. Formal Proofs 2019 (2019) - [j75]Lawrence C. Paulson
, Tobias Nipkow, Makarius Wenzel:
From LCF to Isabelle/HOL. Formal Aspects Comput. 31(6): 675-698 (2019) - [j74]Tobias Nipkow
, Hauke Brinkop
:
Amortized Complexity Verified. J. Autom. Reason. 62(3): 367-391 (2019) - [c95]Peter Lammich
, Tobias Nipkow
:
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. ITP 2019: 23:1-23:18 - [c94]Mohammad Abdulaziz
, Kurt Mehlhorn, Tobias Nipkow:
Trustworthy Graph Algorithms (Invited Talk). MFCS 2019: 1:1-1:22 - [i8]Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel:
From LCF to Isabelle/HOL. CoRR abs/1907.02836 (2019) - [i7]Mohammad Abdulaziz, Kurt Mehlhorn, Tobias Nipkow:
Trustworthy Graph Algorithms. CoRR abs/1907.04065 (2019) - 2018
- [j73]Max W. Haslbeck, Manuel Eberl, Tobias Nipkow:
Treaps. Arch. Formal Proofs 2018 (2018) - [j72]Maximilian P. L. Haslbeck, Tobias Nipkow:
Hoare Logics for Time Bounds. Arch. Formal Proofs 2018 (2018) - [j71]Tobias Nipkow, Stefan Dirix:
Weight-Balanced Trees. Arch. Formal Proofs 2018 (2018) - [j70]Tobias Nipkow, Dániel Somogyi:
Optimal Binary Search Trees. Arch. Formal Proofs 2018 (2018) - [j69]Simon Wimmer, Shuwei Hu, Tobias Nipkow:
Monadification, Memoization and Dynamic Programming. Arch. Formal Proofs 2018 (2018) - [c93]Lars Hupel
, Tobias Nipkow
:
A Verified Compiler from Isabelle/HOL to CakeML. ESOP 2018: 999-1026 - [c92]Manuel Eberl
, Max W. Haslbeck
, Tobias Nipkow
:
Verified Analysis of Random Binary Tree Structures. ITP 2018: 196-214 - [c91]Simon Wimmer
, Shuwei Hu
, Tobias Nipkow
:
Verified Memoization and Dynamic Programming. ITP 2018: 579-596 - [c90]Maximilian P. L. Haslbeck
, Tobias Nipkow
:
Hoare Logics for Time Bounds - A Study in Meta Theory. TACAS (1) 2018: 155-171 - 2017
- [j68]Julius Michaelis, Tobias Nipkow:
Propositional Proof Systems. Arch. Formal Proofs 2017 (2017) - [j67]Tobias Nipkow:
Root-Balanced Tree. Arch. Formal Proofs 2017 (2017) - [c89]Tobias Nipkow
:
Verified Root-Balanced Trees. APLAS 2017: 255-272 - [c88]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: 50-66 - [c87]Julius Michaelis, Tobias Nipkow:
Formalized Proof Systems for Propositional Logic. TYPES 2017: 5:1-5:16 - [p3]Dirk Beyer
, Rolf Hennicker, Martin Hofmann, Tobias Nipkow, Martin Wirsing:
Software-Verifikation. 50 Jahre Universitäts-Informatik in München 2017: 75-86 - [i6]Manuel Eberl, Johannes Hölzl
, Tobias Nipkow:
A Verified Compiler for Probability Density Functions. CoRR abs/1707.06901 (2017) - 2016
- [j66]Hauke Brinkop, Tobias Nipkow:
Pairing Heap. Arch. Formal Proofs 2016 (2016) - [j65]Maximilian P. L. Haslbeck, Tobias Nipkow:
Analysis of List Update Algorithms. Arch. Formal Proofs 2016 (2016) - [j64]Tobias Nipkow:
Abstract Interpretation of Annotated Commands. Arch. Formal Proofs 2016 (2016) - [c86]Maximilian P. L. Haslbeck
, Tobias Nipkow
:
Verified Analysis of List Update Algorithms. FSTTCS 2016: 49:1-49:15 - [c85]Tobias Nipkow
:
Automatic Functional Correctness Proofs for Functional Search Trees. ITP 2016: 307-322 - [c84]Tobias Nipkow:
Verified Analysis of Functional Data Structures. FSCD 2016: 4:1-4:2 - 2015
- [j63]Andreas Lochbihler, Tobias Nipkow:
Trie. Arch. Formal Proofs 2015 (2015) - [j62]Tobias Nipkow:
Parameterized Dynamic Tables. Arch. Formal Proofs 2015 (2015) - [j61]Dmitriy Traytel
, Tobias Nipkow
:
Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. 25 (2015) - [c83]Manuel Eberl
, Johannes Hölzl
, Tobias Nipkow
:
A Verified Compiler for Probability Density Functions. ESOP 2015: 80-104 - [c82]Tobias Nipkow
:
Amortized Complexity Verified. ITP 2015: 310-324 - [c81]Jasmin Christian Blanchette, Max W. Haslbeck
, Daniel Matichuk, Tobias Nipkow
:
Mining the Archive of Formal Proofs. CICM 2015: 3-17 - [i5]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 abs/1501.02155 (2015) - 2014
- [b4]Tobias Nipkow, Gerwin Klein
:
Concrete Semantics - With Isabelle/HOL. Springer 2014, ISBN 978-3-319-10541-3, pp. 1-280 - [j60]Manuel Eberl, Johannes Hölzl, Tobias Nipkow:
A Verified Compiler for Probability Density Functions. Arch. Formal Proofs 2014 (2014) - [j59]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) - [j58]Tobias Nipkow:
Boolean Expression Checkers. Arch. Formal Proofs 2014 (2014) - [j57]Tobias Nipkow:
Amortized Complexity Verified. Arch. Formal Proofs 2014 (2014) - [j56]Tobias Nipkow:
Splay Tree. Arch. Formal Proofs 2014 (2014) - [j55]Tobias Nipkow:
Skew Heap. Arch. Formal Proofs 2014 (2014) - [j54]Tobias Nipkow:
Priority Queues Based on Braun Trees. Arch. Formal Proofs 2014 (2014) - [j53]Tobias Nipkow, Dmitriy Traytel:
Unified Decision Procedures for Regular Expression Equivalence. Arch. Formal Proofs 2014 (2014) - [j52]Dmitriy Traytel, Tobias Nipkow:
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions. Arch. Formal Proofs 2014 (2014) - [j51]Tobias Nipkow, Andrei Popescu:
Making security type systems less ad hoc. it Inf. Technol. 56(6): 267-272 (2014) - [c80]Jasmin Christian Blanchette, Lars Hupel
, Tobias Nipkow
, Lars Noschinski, Dmitriy Traytel
:
Experience report: the next 1100 Haskell programmers. Haskell 2014: 25-30 - [c79]Tobias Nipkow
, Dmitriy Traytel
:
Unified Decision Procedures for Regular Expression Equivalence. ITP 2014: 450-466 - [p2]Gerwin Klein, Tobias Nipkow:
Applications of Interactive Proof to Data Flow Analysis and Security. Software Systems Safety 2014: 77-134 - 2013
- [j50]Andrei Popescu, Johannes Hölzl
, Tobias Nipkow:
Formal Verification of Language-Based Concurrent Noninterference. J. Formaliz. Reason. 6(1): 1-30 (2013) - [c78]Andrei Popescu, Johannes Hölzl
, Tobias Nipkow:
Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. CALCO 2013: 236-252 - [c77]Javier Esparza
, Peter Lammich, René Neumann, Tobias Nipkow
, Alexander Schimpf, Jan-Georg Smaus:
A Fully Verified Executable LTL Model Checker. CAV 2013: 463-478 - [c76]Andrei Popescu, Johannes Hölzl
, Tobias Nipkow
:
Formalizing Probabilistic Noninterference. CPP 2013: 259-275 - [c75]Dmitriy Traytel
, Tobias Nipkow
:
Verified decision procedures for MSO on words based on derivatives of regular expressions. ICFP 2013: 3-12 - [c74]Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow
:
Data Refinement in Isabelle/HOL. ITP 2013: 100-115 - [c73]Tobias Nipkow
, Maximilian P. L. Haslbeck
:
A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions. TABLEAUX 2013: 10-12 - [i4]Nikolaj S. Bjørner, Reiner Hähnle, Tobias Nipkow, Christoph Weidenbach:
Deduction and Arithmetic (Dagstuhl Seminar 13411). Dagstuhl Reports 3(10): 1-24 (2013) - 2012
- [j49]Johannes Hölzl, Tobias Nipkow:
Markov Models. Arch. Formal Proofs 2012 (2012) - [j48]Alexander Krauss, Tobias Nipkow
:
Proof Pearl: Regular Expression Equivalence and Relation Algebra. J. Autom. Reason. 49(1): 95-106 (2012) - [j47]Klaus Aehlig, Florian Haftmann, Tobias Nipkow
:
A compiled implementation of normalisation by evaluation. J. Funct. Program. 22(1): 9-30 (2012) - [c72]Andrei Popescu, Johannes Hölzl
, Tobias Nipkow
:
Proving Concurrent Noninterference. CPP 2012: 109-125 - [c71]Tobias Nipkow
:
Abstract Interpretation of Annotated Commands. ITP 2012: 116-132 - [c70]Johannes Hölzl, Tobias Nipkow
:
Verifying pCTL Model Checking. TACAS 2012: 347-361 - [c69]Tobias Nipkow
:
Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs. VMCAI 2012: 24-38 - [c68]Johannes Hölzl
, Tobias Nipkow:
Interactive verification of Markov chains: Two distributed protocol case studies. QFM 2012: 17-31 - [p1]Tobias Nipkow:
Interactive Proof: Introduction to Isabelle/HOL. Software Safety and Security 2012: 254-285 - [e9]Tobias Nipkow, Orna Grumberg, Benedikt Hauptmann:
Software Safety and Security - Tools for Analysis and Verification. NATO Science for Peace and Security Series - D: Information and Communication Security 33, IOS Press 2012, ISBN 978-1-61499-027-7 [contents] - 2011
- [j46]Tobias Nipkow:
Gauss-Jordan Elimination for Matrices Represented as Functions. Arch. Formal Proofs 2011 (2011) - [j45]Tobias Nipkow:
Majority Vote Algorithm Revisited Again. Int. J. Softw. Informatics 5(1-2): 21-28 (2011) - [c67]Dmitriy Traytel
, Stefan Berghofer, Tobias Nipkow
:
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. APLAS 2011: 89-104 - [c66]Dongchen Jiang, Tobias Nipkow
:
Proof Pearl: The Marriage Theorem. CPP 2011: 394-399 - [c65]Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow
:
Automatic Proof and Disproof in Isabelle/HOL. FroCoS 2011: 12-27 - [c64]Tobias Nipkow
:
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. ITP 2011: 281-296 - 2010
- [j44]Dongchen Jiang, Tobias Nipkow:
Hall's Marriage Theorem. Arch. Formal Proofs 2010 (2010) - [j43]Alexander Krauss, Tobias Nipkow:
Regular Sets and Expressions. Arch. Formal Proofs 2010 (2010) - [j42]Tobias Nipkow:
List Index. Arch. Formal Proofs 2010 (2010) - [j41]Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow
, Steven Obua, Roland Zumkeller:
A Revision of the Proof of the Kepler Conjecture. Discret. Comput. Geom. 44(1): 1-34 (2010) - [j40]Franz Baader
, Bernhard Beckert, Tobias Nipkow
:
Deduktion: von der Theorie zur Anwendung. Inform. Spektrum 33(5): 444-451 (2010) - [j39]Tobias Nipkow
:
Linear Quantifier Elimination. J. Autom. Reason. 45(2): 189-212 (2010) - [c63]Sascha Böhme, Tobias Nipkow
:
Sledgehammer: Judgement Day. IJCAR 2010: 107-121 - [c62]Florian Haftmann, Tobias Nipkow
:
Code Generation via Higher-Order Rewrite Systems. FLOPS 2010: 103-117 - [c61]Jasmin Christian Blanchette, Tobias Nipkow
:
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. ITP 2010: 131-146
2000 – 2009
- 2009
- [j38]Steven Obua, Tobias Nipkow
:
Flyspeck II: the basic linear programs. Ann. Math. Artif. Intell. 56(3-4): 245-272 (2009) - [j37]Tobias Nipkow
:
Social Choice Theory in HOL. J. Autom. Reason. 43(3): 289-304 (2009) - [e8]Thomas Ball, Jürgen Giesl, Reiner Hähnle, Tobias Nipkow:
Interaction versus Automation: The two Faces of Deduction, 04.10. - 09.10.2009. Dagstuhl Seminar Proceedings 09411, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany 2009 [contents] - [e7]Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel:
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science 5674, Springer 2009, ISBN 978-3-642-03358-2 [contents] - [i3]Thomas Ball, Jürgen Giesl, Reiner Hähnle, Tobias Nipkow:
09411 Abstracts Collection - Interaction versus Automation: The two Faces of Deduction. Interaction versus Automation: The two Faces of Deduction 2009 - [i2]Thomas Ball, Jürgen Giesl, Reiner Hähnle, Tobias Nipkow:
09411 Executive Summary - Interaction versus Automation: The two Faces of Deductions. Interaction versus Automation: The two Faces of Deduction 2009 - 2008
- [j36]Klaus Aehlig, Tobias Nipkow:
Normalization by Evaluation. Arch. Formal Proofs 2008 (2008) - [j35]Tobias Nipkow:
Quantifier Elimination for Linear Arithmetic. Arch. Formal Proofs 2008 (2008) - [j34]Tobias Nipkow:
Fun With Functions. Arch. Formal Proofs 2008 (2008) - [j33]Tobias Nipkow:
Arrow and Gibbard-Satterthwaite. Arch. Formal Proofs 2008 (2008) - [j32]Tobias Nipkow, Lawrence C. Paulson:
Fun With Tilings. Arch. Formal Proofs 2008 (2008) - [j31]Amine Chaieb, Tobias Nipkow
:
Proof Synthesis and Reflection for Linear Arithmetic. J. Autom. Reason. 41(1): 33-59 (2008) - [j30]Serge Autexier
, Heiko Mantel, Stephan Merz, Tobias Nipkow
:
Preface. J. Autom. Reason. 41(3-4): 191-192 (2008) - [c60]Tobias Nipkow
:
Linear Quantifier Elimination. IJCAR 2008: 18-33 - [c59]Makarius Wenzel, Lawrence C. Paulson
, Tobias Nipkow:
The Isabelle Framework. TPHOLs 2008: 33-38 - [c58]Klaus Aehlig, Florian Haftmann, Tobias Nipkow:
A Compiled Implementation of Normalization by Evaluation. TPHOLs 2008: 39-54 - 2007
- [c57]Tobias Nipkow:
Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic. VERIFY 2007 - [c56]Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip:
C++ ist typsicher? Garantiert! Software Engineering 2007: 29-31 - [c55]Lukas Bulwahn, Alexander Krauss, Tobias Nipkow:
Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. TPHOLs 2007: 38-53 - [e6]Stephan Merz, Tobias Nipkow:
Proceedings of the 6th International Workshop on Automated Verification of Critical Systems, AVoCS 2006, Nancy, France, September 18-19, 2006. Electronic Notes in Theoretical Computer Science 185, Elsevier 2007 [contents] - 2006
- [j29]Gertrud Bauer, Tobias Nipkow:
Flyspeck I: Tame Graphs. Arch. Formal Proofs 2006 (2006) - [j28]Tobias Nipkow:
Abstract Hoare Logics. Arch. Formal Proofs 2006 (2006) - [j27]Tobias Nipkow:
Hotel Key Card System. Arch. Formal Proofs 2006 (2006) - [j26]Gerwin Klein
, Tobias Nipkow
:
A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4): 619-695 (2006) - [c54]Tobias Nipkow, Gertrud Bauer, Paula Schultz:
Flyspeck I: Tame Graphs. IJCAR 2006: 21-35 - [c53]Tobias Nipkow:
Verifying a Hotel Key Card System. ICTAC 2006: 1-14 - [c52]Daniel Wasserrab, Tobias Nipkow
, Gregor Snelting, Frank Tip:
An operational semantics and type safety prooffor multiple inheritance in C++. OOPSLA 2006: 345-362 - [c51]Stephan Merz, Tobias Nipkow
:
Preface. AVoCS 2006: 1-2 - [e5]Jayadev Misra, Tobias Nipkow, Emil Sekerinski:
FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings. Lecture Notes in Computer Science 4085, Springer 2006, ISBN 3-540-37215-6 [contents] - 2005
- [j25]Gerwin Klein, Tobias Nipkow:
Jinja is not Java. Arch. Formal Proofs 2005 (2005) - [j24]Farhad Mehta, Tobias Nipkow
:
Proving pointer programs in higher-order logic. Inf. Comput. 199(1-2): 200-227 (2005) - [c50]Martin Wildmoser, Tobias Nipkow:
Asserting Bytecode Safety. ESOP 2005: 326-341 - [c49]Amine Chaieb, Tobias Nipkow
:
Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. LPAR 2005: 367-380 - [c48]Tobias Nipkow, Lawrence C. Paulson:
Proof Pearl: Defining Functions over Finite Sets. TPHOLs 2005: 385-396 - [c47]Martin Wildmoser, Amine Chaieb, Tobias Nipkow
:
Bytecode Analysis for Proof Carrying Code. Bytecode@ETAPS 2005: 19-34 - [i1]Tobias Nipkow, Gertrud Bauer:
Towards a Verified Enumeration of All Tame Plane Graphs. Mathematics, Algorithms, Proofs 2005 - 2004
- [j23]Wolfgang Naraschewski, Tobias Nipkow:
Mini ML. Arch. Formal Proofs 2004 (2004) - [j22]Tobias Nipkow:
Functional Automata. Arch. Formal Proofs 2004 (2004) - [j21]Tobias Nipkow:
Compiling Exceptions Correctly. Arch. Formal Proofs 2004 (2004) - [j20]Tobias Nipkow, Cornelia Pusch:
AVL Trees. Arch. Formal Proofs 2004 (2004) - [c46]Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz:
Prototyping Proof Carrying Code. IFIP TCS 2004: 333-347 - [c45]Stefan Berghofer, Tobias Nipkow:
Random Testing in Isabelle/HOL. SEFM 2004: 230-239 - [c44]Martin Wildmoser, Tobias Nipkow:
Certifying Machine Code Safety: Shallow Versus Deep Embedding. TPHOLs 2004: 305-320 - 2003
- [j19]Tobias Nipkow:
Java Bytecode Verification. J. Autom. Reason. 30(3-4): 233 (2003) - [j18]Gerwin Klein
, Tobias Nipkow
:
Verified bytecode verifiers. Theor. Comput. Sci. 298(3): 583-626 (2003) - [c43]Farhad Mehta, Tobias Nipkow:
Proving Pointer Programs in Higher-Order Logic. CADE 2003: 121-135 - 2002
- [b3]Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel:
Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283, Springer 2002, ISBN 3-540-43376-7 - [c42]Tobias Nipkow:
Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. CSL 2002: 103-119 - [c41]David von Oheimb, Tobias Nipkow:
Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. FME 2002: 89-105 - [c40]Gertrud Bauer, Tobias Nipkow:
The 5 Colour Theorem in Isabelle/Isar. TPHOLs 2002: 67-82 - [c39]Tobias Nipkow:
Structured Proofs in Isar/HOL. TYPES 2002: 259-278 - 2001
- [j17]Gerwin Klein
, Tobias Nipkow
:
Verified lightweight bytecode verification. Concurr. Comput. Pract. Exp. 13(13): 1133-1151 (2001) - [j16]Tobias Nipkow
:
More Church-Rosser Proofs. J. Autom. Reason. 26(1): 51-66 (2001) - [c38]Tobias Nipkow:
Verified Bytecode Verifiers. FoSSaCS 2001: 347-363 - [e4]Rajeev Goré, Alexander Leitsch, Tobias Nipkow:
Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings. Lecture Notes in Computer Science 2083, Springer 2001, ISBN 3-540-42254-4 [contents] - 2000
- [j15]Tobias Nipkow:
Preface. Inf. Comput. 159(1-2): 1 (2000) - [c37]Martin Wirsing, Martin Gogolla, Hans-Jörg Kreowski, Tobias Nipkow, Wolfgang Reif:
Workshop über Rigorose Entwicklung software-intensiver Systeme. GI Jahrestagung 2000: 465-466 - [c36]Stefan Berghofer, Tobias Nipkow:
Proof Terms for Simply Typed Higher Order Logic. TPHOLs 2000: 38-52 - [c35]Stefan Berghofer, Tobias Nipkow:
Executing Higher Order Logic. TYPES 2000: 24-40
1990 – 1999
- 1999
- [j14]Wolfgang Naraschewski, Tobias Nipkow:
Type Inference Verified: Algorithm W in Isabelle/HOL. J. Autom. Reason. 23(3-4): 299-318 (1999) - [j13]Olaf Müller, Tobias Nipkow
, David von Oheimb, Oscar Slotosch:
HOLCF=HOL+LCF. J. Funct. Program. 9(2): 191-223 (1999) - [c34]Tobias Nipkow
:
Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract). CADE 1999: 398 - [c33]Tobias Nipkow, Leonor Prensa Nieto:
Owicki/Gries in Isabelle/HOL. FASE 1999: 188-203 - [c32]David von Oheimb, Tobias Nipkow:
Machine-Checking the Java Specification: Proving Type-Safety. Formal Syntax and Semantics of Java 1999: 119-156 - 1998
- [b2]Franz Baader, Tobias Nipkow:
Term rewriting and all that. Cambridge University Press 1998, ISBN 978-0-521-45520-6, pp. I-XII, 1-301 - [j12]Tobias Nipkow:
Winskel is (almost) Right: Towards a Mechanized Semantics. Formal Aspects Comput. 10(2): 171-186 (1998) - [j11]Richard Mayr, Tobias Nipkow
:
Higher-Order Rewrite Systems and Their Confluence. Theor. Comput. Sci. 192(1): 3-29 (1998) - [c31]Tobias Nipkow, David von Oheimb:
Javalight is Type-Safe - Definitely. POPL 1998: 161-170 - [c30]Tobias Nipkow:
Verified Lexical Analysis. TPHOLs 1998: 1-15 - [e3]Tobias Nipkow
:
Rewriting Techniques and Applications, 9th International Conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998, Proceedings. Lecture Notes in Computer Science 1379, Springer 1998, ISBN 3-540-64301-X [contents] - 1997
- [c29]Olaf Müller, Tobias Nipkow:
Traces of I/O-Automata in Isabelle/HOLCF. TAPSOFT 1997: 580-594 - 1996
- [c28]Tobias Nipkow
:
More Church-Rosser Proofs (in Isabelle/HOL). CADE 1996: 733-747 - [c27]Tobias Nipkow:
Winskel is (Almost) Right: Towards a Mechanized Semantics Textbook. FSTTCS 1996: 180-192 - [c26]Dieter Nazareth, Tobias Nipkow:
Formal Verification of Algorithm W: The Monomorphic Case. TPHOLs 1996: 331-345 - [c25]Wolfgang Naraschewski, Tobias Nipkow
:
Type Inference Verified: Algorithm W in Isabelle/HOL. TYPES 1996: 317-332 - 1995
- [j10]Tobias Nipkow
, Christian Prehofer:
Type Reconstruction for Type Classes. J. Funct. Program. 5(2): 201-224 (1995) - [c24]Tobias Nipkow:
Higher-Order Rewrite Systems (Abstract). RTA 1995: 256 - [c23]Olaf Müller, Tobias Nipkow:
Combining Model Checking and Deduction for I/O-Automata. TACAS 1995: 1-16 - 1994
- [j9]Zhenyu Qian, Tobias Nipkow
:
Reduction and Unification in Lambda Calculi with a General Notion of Subtype. J. Autom. Reason. 12(3): 389-406 (1994) - [c22]Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, Birgit Schieder:
Interpreter Verification for a Functional Language. FSTTCS 1994: 77-88 - [c21]Tobias Nipkow, Konrad Slind:
I/Q Automata in Isabelle/HOL. TYPES 1994: 101-119 - [e2]Jan Heering, Karl Meinke, Bernhard Möller, Tobias Nipkow:
Higher-Order Algebra, Logic, and Term Rewriting, First International Workshop, HOA '93, Amsterdam, The Netherlands, September 23-24, 1993, Selected Papers. Lecture Notes in Computer Science 816, Springer 1994, ISBN 3-540-58233-9 [contents] - [e1]Henk Barendregt, Tobias Nipkow:
Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers. Lecture Notes in Computer Science 806, Springer 1994, ISBN 3-540-58085-9 [contents] - 1993
- [c20]Tobias Nipkow:
Functional Unification of Higher-Order Patterns. LICS 1993: 64-74 - [c19]Tobias Nipkow, Christian Prehofer:
Type Checking Type Classes. POPL 1993: 409-418 - [c18]Tobias Nipkow:
Orthogonal Higher-Order Rewrite Systems are Confluent. TLCA 1993: 306-317 - 1992
- [c17]Tobias Nipkow, Zhenyu Qian:
Reduction and Unification in Lambda Calculi with Subtypes. CADE 1992: 66-78 - [c16]Tobias Nipkow, Lawrence C. Paulson
:
Isabelle-91. CADE 1992: 673-676 - 1991
- [j8]Tobias Nipkow
:
Constructive Rewriting. Comput. J. 34(1): 34-41 (1991) - [j7]Tobias Nipkow
:
Combining Matching Algorithms: The Regular Case. J. Symb. Comput. 12(6): 633-654 (1991) - [c15]Tobias Nipkow
, Gregor Snelting:
Type Classes and Overloading Resolution via Order-Sorted Unification. FPCA 1991: 1-14 - [c14]Tobias Nipkow:
Higher-Order Critical Pairs. LICS 1991: 342-349 - [c13]Tobias Nipkow
, Zhenyu Qian:
Modular Higher-Order E-Unification. RTA 1991: 200-214 - 1990
- [j6]Tobias Nipkow
:
Unification in Primal Algebras, Their Powers and Their Varieties. J. ACM 37(4): 742-776 (1990) - [c12]Ursula Martin
, Tobias Nipkow
:
Ordered Rewriting and Confluence. CADE 1990: 366-380 - [c11]Tobias Nipkow
:
Higher-Order Unification, Polymorphism, and Subsorts (Extended Abstract). CTRS 1990: 436-447 - [c10]Ursula Martin, Tobias Nipkow:
Automating Squiggol. Programming Concepts and Methods 1990: 233-246 - [c9]Tobias Nipkow:
Proof Transformations for Equational Theories. LICS 1990: 278-288
1980 – 1989
- 1989
- [j5]Tobias Nipkow
:
Term Rewriting and Beyond - Theorem Proving in Isabelle. Formal Aspects Comput. 1(4): 320-338 (1989) - [j4]Ursula Martin
, Tobias Nipkow
:
Boolean Unification - The Story So Far. J. Symb. Comput. 7(3/4): 275-293 (1989) - [j3]Tobias Nipkow
:
Equational Reasoning in Isabelle. Sci. Comput. Program. 12(2): 123-149 (1989) - [c8]Tobias Nipkow
:
Formal Verification of Data Type Refinement - Theory and Practice. REX Workshop 1989: 561-591 - [c7]Tobias Nipkow
:
Combining Matching Algorithms: The Rectangular Case. RTA 1989: 343-358 - 1988
- [j2]Ursula Martin
, Tobias Nipkow
:
Unification in Boolean Rings. J. Autom. Reason. 4(4): 381-396 (1988) - [c6]Tobias Nipkow
:
Unification in Primal Algebras. CAAP 1988: 117-131 - 1987
- [c5]Tobias Nipkow
:
Observing Non-Deterministic Data Types. ADT 1987: 170-183 - [c4]Tobias Nipkow
:
Are Homomorphisms Sufficient for Behavioural Implementations of Deterministic and Nondeterministic Data Types? STACS 1987: 260-271 - 1986
- [b1]Tobias Nipkow:
Behavioural implementation concepts for nondeterministic data types. University of Manchester, UK, 1986 - [j1]Tobias Nipkow
:
Non-deterministic Data Types: Models and Implementations. Acta Informatica 22(6): 629-661 (1986) - [c3]Tobias Nipkow:
Behavioural Implementations of Non-Deterministic Data Types. ADT 1986 - [c2]Ursula Martin
, Tobias Nipkow
:
Unification in Boolean Rings. CADE 1986: 506-513 - 1983
- [c1]Tobias Nipkow, Gerhard Weikum:
A decidability result about sufficient-completeness of axiomatically specified abstract data types. Theoretical Computer Science 1983: 257-268
Coauthor Index
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-05 21:14 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint