default search action
Tobias Nipkow
Person information
- affiliation: Technical University Munich, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
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) - [c108]Tobias Nipkow:
Region Quadtrees Verified. Taming the Infinities of Concurrency 2024: 243-254 - [c107]Tobias Nipkow:
Alpha-Beta Pruning Verified (Invited Talk). ITP 2024: 1:1-1:4 - [c106]Martin Rau, Tobias Nipkow:
A Verified Earley Parser. ITP 2024: 31:1-31:18 - 2023
- [j85]Simon Roßkopf
A Formalization and Proof Checker for Isabelle's Metalogic. J. Autom. Reason. 67(1): 1 (2023) - [c105]Katharina Kreuzer
Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. CADE 2023: 365-381 - [c104]Balázs Tóth
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
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
A Verified Decision Procedure for Orders in Isabelle/HOL. ATVA 2021: 127-143 - [c101]Tobias Nipkow
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
Verified Analysis of Random Binary Tree Structures. J. Autom. Reason. 64(5): 879-910 (2020) - [c99]Tobias Nipkow
Verified Textbook Algorithms - A Biased Survey. ATVA 2020: 25-53 - [c98]Robin Eßmann
Verified Approximation Algorithms. IJCAR (2) 2020: 291-306 - [c97]Martin Rau
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
From LCF to Isabelle/HOL. Formal Aspects Comput. 31(6): 675-698 (2019) - [j74]Tobias Nipkow
Amortized Complexity Verified. J. Autom. Reason. 62(3): 367-391 (2019) - [c95]Peter Lammich
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
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
A Verified Compiler from Isabelle/HOL to CakeML. ESOP 2018: 999-1026 - [c92]Manuel Eberl
Verified Analysis of Random Binary Tree Structures. ITP 2018: 196-214 - [c91]Simon Wimmer
Verified Memoization and Dynamic Programming. ITP 2018: 579-596 - [c90]Maximilian P. L. Haslbeck
Hoare Logics for Time Bounds - A Study in Meta Theory. TACAS (1) 2018: 155-171 - [d1]Lars Hupel
A Verified Compiler from Isabelle/HOL to CakeML. Zenodo, 2018 - 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
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
Software-Verifikation. 50 Jahre Universitäts-Informatik in München 2017: 75-86 - [i6]Manuel Eberl, Johannes Hölzl
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
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
Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. 25 (2015) - [c83]Manuel Eberl
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
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
Experience report: the next 1100 Haskell programmers. Haskell 2014: 25-30 - [c79]Tobias Nipkow
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
Formal Verification of Language-Based Concurrent Noninterference. J. Formaliz. Reason. 6(1): 1-30 (2013) - [c78]Andrei Popescu, Johannes Hölzl
Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. CALCO 2013: 236-252 - [c77]Javier Esparza
A Fully Verified Executable LTL Model Checker. CAV 2013: 463-478 - [c76]Andrei Popescu, Johannes Hölzl
Formalizing Probabilistic Noninterference. CPP 2013: 259-275 - [c75]Dmitriy Traytel
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
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
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
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
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
A Revision of the Proof of the Kepler Conjecture. Discret. Comput. Geom. 44(1): 1-34 (2010) - [j40]Franz Baader
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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-10-07 22:10 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: