Tobias Nipkow
#17,234
Most Influential Person Now
German computer scientist
Tobias Nipkow's AcademicInfluence.com Rankings
Tobias Nipkowcomputer-science Degrees
Computer Science
#879
World Rank
#911
Historical Rank
Programming
#41
World Rank
#43
Historical Rank
Database
#1903
World Rank
#1996
Historical Rank
Download Badge
Computer Science
Why Is Tobias Nipkow Influential?
(Suggest an Edit or Addition)According to Wikipedia, Tobias Nipkow is a German computer scientist. Career Nipkow received his Diplom in computer science from the Department of Computer Science of the Technische Hochschule Darmstadt in 1982, and his Ph.D. from the University of Manchester in 1987.
Tobias Nipkow's Published Works
Number of citations in a given year to any of this author's works
Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author
Published Works
- Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002) (2644)
- Isabelle: A Generic Theorem Prover (1994) (1360)
- Term rewriting and all that (1998) (1293)
- A Proof Assistant for Higher-Order Logic (2002) (932)
- Isabelle/HOL (2002) (477)
- A FORMAL PROOF OF THE KEPLER CONJECTURE (2015) (368)
- Higher-order critical pairs (1991) (318)
- A machine-checked model for a Java-like language, virtual machine, and compiler (2006) (292)
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (2010) (283)
- Javalight is type-safe—definitely (1998) (194)
- Higher-Order Rewrite Systems and Their Confluence (1998) (191)
- Code Generation via Higher-Order Rewrite Systems (2010) (188)
- Concrete Semantics: With Isabelle/HOL (2014) (171)
- The Isabelle Framework (2008) (164)
- Proving pointer programs in higher-order logic (2005) (158)
- FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings (2006) (147)
- Sledgehammer: Judgement Day (2010) (134)
- Verified Bytecode Verifiers (2001) (128)
- A Revision of the Proof of the Kepler Conjecture (2009) (126)
- Winskel is (almost) Right: Towards a Mechanized Semantics Textbook (1996) (123)
- Executing Higher Order Logic (2000) (121)
- Random testing in Isabelle/HOL (2004) (119)
- Machine-Checking the Java Specification: Proving Type-Safety (1999) (117)
- Boolean Unification - The Story So Far (1989) (104)
- Automatic Proof and Disproof in Isabelle/HOL (2011) (102)
- Functional unification of higher-order patterns (1993) (95)
- Theorem Proving in Higher Order Logics (1998) (95)
- A Fully Verified Executable LTL Model Checker (2013) (85)
- Structured Proofs in Isar/HOL (2002) (83)
- Combining Model Checking and Deduction for I/O-Automata (1995) (78)
- HOLCF = HOL + LCF (1999) (78)
- Certifying Machine Code Safety: Shallow Versus Deep Embedding (2004) (76)
- Isabelle tutorial and user’s manual (1990) (74)
- Ordered Rewriting and Confluence (1990) (74)
- Data Refinement in Isabelle/HOL (2013) (71)
- Proof Terms for Simply Typed Higher Order Logic (2000) (71)
- The Isabelle Reference Manual (2007) (69)
- Hoare Logics for Recursive Procedures and Unbounded Nondeterminism (2002) (67)
- Type Classes and Overloading Resolution via Order-Sorted Unification (1991) (67)
- Hoare Logics in Isabelle/HOL (2002) (66)
- More Church-Rosser Proofs (in Isabelle/HOL) (1996) (66)
- Mujava: embedding a programming language in a theorem prover (1999) (65)
- Proof Pearl: Regular Expression Equivalence and Relation Algebra (2012) (64)
- Orthogonal Higher-Order Rewrite Systems are Confluent (1993) (63)
- Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited (2002) (61)
- Combining Matching Algorithms: The Regular Case (1991) (61)
- Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL (2017) (60)
- Flyspeck I: Tame Graphs (2006) (59)
- Type Reconstruction for Type Classes (1995) (55)
- Order-sorted polymorphism in Isabelle (1993) (54)
- Linear Quantifier Elimination (2008) (53)
- Probabilistic Models (2004) (53)
- Concrete Semantics (2014) (51)
- A Code Generator Framework for Isabelle / HOL (2007) (49)
- Type checking type classes (1993) (47)
- I/Q Automata in Isabelle/HOL (1994) (46)
- A Verified Compiler from Isabelle/HOL to CakeML (2018) (46)
- Mining the Archive of Formal Proofs (2015) (45)
- Type Inference Verified: Algorithm W in Isabelle/HOL (1996) (45)
- Verified lightweight bytecode verification (2001) (44)
- A decidability result about sufficient-completeness of axiomatically specified abstract data types (1983) (42)
- Higher-Order Algebra, Logic, and Term Rewriting (1993) (42)
- Social Choice Theory in HOL (2009) (41)
- Non-deterministic data types: models and implementations (1986) (41)
- Equational Reasoning in Isabelle (1989) (40)
- An operational semantics and type safety prooffor multiple inheritance in C++ (2006) (40)
- More Church–Rosser Proofs (2004) (39)
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL (2007) (38)
- Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings (2009) (36)
- Owicki/Gries in Isabelle/HOL (1999) (35)
- Flyspeck II: the basic linear programs (2009) (35)
- Amortized Complexity Verified (2015) (35)
- Proof transformations for equational theories (1990) (34)
- Isabelle-91 (1992) (34)
- Proof Synthesis and Reflection for Linear Arithmetic (2008) (33)
- Social Choice Theory in HOL Arrow and Gibbard-Satterthwaite (2009) (33)
- Bytecode Analysis for Proof Carrying Code (2005) (32)
- Unification in primal algebras, their powers and their varieties (1990) (32)
- Normalization by Evaluation (2008) (31)
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic (2005) (31)
- Prototyping Proof Carrying Code (2004) (29)
- Verified Lexical Analysis (1998) (29)
- Higher-Order Unification, Polymorphism, and Subsorts (Extended Abstract) (1990) (26)
- Traces of I/O-Automata in Isabelle/HOLCF (1997) (26)
- A Compiled Implementation of Normalization by Evaluation (2008) (24)
- Modular Higher-Order E-Unification (1991) (24)
- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs (2012) (23)
- Formal Verification of Algorithm W: The Monomorphic Case (1996) (23)
- A Tutorial Introduction to Structured Isar Proofs (2008) (22)
- Unified Decision Procedures for Regular Expression Equivalence (2014) (22)
- Jinja: Towards a Comprehensive Formal Semantics for a Java-like Language (2003) (22)
- From LCF to Isabelle/HOL (2019) (22)
- Extending Hindley-Milner Type Inference with Coercive Structural Subtyping (2011) (21)
- Asserting Bytecode Safety (2005) (20)
- Software Safety and Security - Tools for Analysis and Verification (2012) (20)
- Behavioural implementation concepts for nondeterministic data types (1986) (20)
- Proof Pearl: Defining Functions over Finite Sets (2005) (20)
- Formal Logical Methods for System Security and Correctness (2008) (20)
- Proving Concurrent Noninterference (2012) (19)
- Veried Bytecode Veriers (2002) (19)
- The 5 Colour Theorem in Isabelle/Isar (2002) (19)
- A Verified Compiler for Probability Density Functions (2015) (18)
- Automatic Functional Correctness Proofs for Functional Search Trees (2016) (16)
- Verifying a Hotel Key Card System (2006) (16)
- Term rewriting and beyond — theorem proving in Isabelle (1989) (15)
- Formalizing Probabilistic Noninterference (2013) (15)
- Reduction and Unification in Lambda Calculi with Subtypes (1992) (15)
- Java Bytecode Verification (2003) (14)
- Formal Verification of Data Type Refinement - Theory and Practice (1989) (14)
- Verified decision procedures for MSO on words based on derivatives of regular expressions (2013) (14)
- Observing Non-Deterministic Data Types (1988) (13)
- Formalized Proof Systems for Propositional Logic (2017) (13)
- Jinja is not Java (2005) (12)
- Types for Proofs and Programs: International Workshop TYPES '93, Nijmegen, The Netherlands, May 24 - 28, 1993. Selected Papers (1994) (12)
- Combining Matching Algorithms: The Rectangular Case (1989) (12)
- Hoare Logics for Time Bounds - A Study in Meta Theory (2018) (12)
- Are Homomorphisms Sufficient for Behavioural Implementations of Deterministic and Nondeterministic Data Types? (1987) (11)
- Verifying pCTL Model Checking (2012) (11)
- Programming and Proving (2013) (11)
- From Semantics to Computer Science (2009) (11)
- Propositional Proof Systems (2017) (11)
- Verified Root-Balanced Trees (2017) (11)
- Abstract Interpretation of Annotated Commands (2012) (11)
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism (2011) (10)
- Interactive verification of Markov chains: Two distributed protocol case studies (2012) (10)
- Verified Textbook Algorithms - A Biased Survey (2020) (10)
- Generic Proof Synthesis for Presburger Arithmetic (2003) (10)
- Unification in Boolean rings (1986) (10)
- Journal of Automated Reasoning Special Issue: Formal Modeling and Verification of Critical Systems (2008) (9)
- Unification in Primal Algebras (1988) (9)
- Automating Squiggol (1990) (9)
- Verified Analysis of Random Binary Tree Structures (2018) (8)
- From Semantics to Computer Science: Nominal verification of algorithm W (2009) (8)
- Interpreter Verification for a Functional Language (1994) (7)
- Isabelle's Logics: HOL1 (2000) (7)
- Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference (2013) (7)
- Optimal Binary Search Trees (2018) (7)
- Java Source and Bytecode Formalizations in Isabelle: Java (2002) (7)
- Gauss-Jordan Elimination for Matrices Represented as Functions (2011) (7)
- Isabelle's Metalogic: Formalization and Proof Checker (2021) (7)
- Arrow and Gibbard-Satterthwaite (2008) (7)
- The supplemental Isabelle/HOL library (2002) (6)
- Isabelle HOL - The Tutorial (2000) (6)
- Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (2009) (6)
- 1. The Basics (2002) (6)
- Reflecting Quantifier Elimination for Linear Arithmetic (2008) (6)
- Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra (2019) (5)
- Abstract Hoare Logics (2006) (5)
- Formal Verification of Language-Based Concurrent Noninterference (2013) (5)
- Regular Sets and Expressions (2010) (5)
- Verified Memoization and Dynamic Programming (2018) (5)
- Constructive Rewriting (1991) (5)
- AVL Trees (2004) (5)
- Proceedings of the international workshop on Types for proofs and programs (1994) (5)
- Logic and computation—Interactive proof with Cambridge LCF: By L.C. Paulson. Cambridge University Press, Cambridge, 1987, Price £27.50, ISBN 0 521 34632 0 (1988) (4)
- Trustworthy Graph Algorithms (Invited Talk) (2019) (4)
- Teaching algorithms and data structures with a proof assistant (invited talk) (2021) (4)
- Hall's Marriage Theorem (2010) (4)
- Reduction and unification in lambda calculi with a general notion of subtype (1994) (4)
- Types for Proofs and Programs (1994) (4)
- IMP: A Simple Imperative Language (2014) (4)
- Interactive Proof: Introduction to Isabelle/HOL (2012) (4)
- Mule: A support system for formal specification and rigorous software development (1983) (4)
- Automated Reasoning First International Joint Conference, Ijcar 2001, Siena, Italy, June 18-23, 2001 : Proceedings (2001) (4)
- Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract) (1999) (4)
- Boolean Expression Checkers (2014) (4)
- Experience report (2014) (3)
- Trustworthy Graph Algorithms (2019) (3)
- Verified Analysis of List Update Algorithms (2016) (3)
- Hoare Logics for Time Bounds (2018) (3)
- A compiled implementation of normalisation by evaluation* (2012) (3)
- Proof Pearl: The Marriage Theorem (2011) (3)
- Priority Search Trees (2019) (3)
- Verified Analysis of Random Trees (2018) (3)
- Interpreter Veriication for a Functional Language (1994) (3)
- Proceedings of the First International Joint Conference on Automated Reasoning (2001) (3)
- Verified Approximation Algorithms (2020) (3)
- Priority Queues Based on Braun Trees (2014) (3)
- Compiling Exceptions Correctly (2004) (2)
- Splay Tree (2014) (2)
- Making security type systems less ad hoc (2014) (2)
- Selected Papers from the Second International Workshop on Higher-Order Algebra, Logic, and Term Rewriting (1993) (2)
- An Operational Semantics and Type Safety Proof for C + +-like Multiple Inheritance (2005) (2)
- Higher-Order Rewrite Systems (Abstract) (1995) (2)
- Verified Analysis of Functional Data Structures (2016) (2)
- Trie (2015) (2)
- 6. Sets, Functions, and Relations (2002) (2)
- Fun With Functions (2008) (2)
- Adding Soft Types to Isabelle (2018) (2)
- Treaps (2018) (2)
- Proof pearl: Braun trees (2020) (1)
- Verified Approximation Algorithms (2022) (1)
- Monadification, Memoization and Dynamic Programming (2018) (1)
- Term Rewriting and All That : Confluence (1998) (1)
- List Index (2010) (1)
- MDB: A Graph-Like Persistent Database (1985) (1)
- Higher-order Rewrite Systems and Their Confluence Higher-order Rewrite Systems and Their Connuence (1994) (1)
- Extending Hindley-Milner Type Inference with Coercive Subtyping ( long version ) (2011) (1)
- Weight-Balanced Trees (2018) (1)
- Parameterized Dynamic Tables (2015) (1)
- FM 2006: Formal Methods: 14th International Symposium on Formal MethodsHamilton, Canada, August 21-27, 2006Proceedings (Lecture Notes in Computer Science) (2006) (1)
- Functional Automata (2004) (1)
- Verification of Closest Pair of Points Algorithms (2020) (1)
- Embedding Programming Languages in Theorem Provers (1999) (1)
- Generic proof synthesis for presburger arithmetic-draft (2004) (1)
- Towards a Verified Enumeration of All Tame Plane Graphs (2005) (1)
- Amortized Complexity Verified (2018) (1)
- Analysis of List Update Algorithms (2016) (1)
- Behavioural Implementations of Non-Deterministic Data Types (1986) (1)
- Pairing Heap (2016) (1)
- Old Isabelle Reference Manual (2009) (1)
- Applications of Interactive Proof to Data Flow Analysis and Security (2014) (1)
- 7. Inductively Defined Sets (2002) (1)
- Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra (2019) (1)
- Markov Models (2019) (1)
- Root-Balanced Tree (2017) (1)
- Rewriting techniques and applications : 9th International Conference, RTA-98, Tsukuba, Japan, March 30-April 1, 1998 : proceedings (1998) (1)
- A Bluffer's Guide to ml (1998) (1)
- A Verified Decision Procedure for Orders in Isabelle/HOL (2021) (1)
- Verified Analysis of Random Binary Tree Structures (2020) (1)
- 5. The Rules of the Game (2002) (1)
- Formalising and Monitoring Traffic Rules for Autonomous Vehicles Involving Multiple Lanes in {Isabelle/HOL} (2017) (0)
- Application for a Dagstuhl Seminar Deduction and Arithmetic (2010) (0)
- Fun With Tilings (2008) (0)
- Isabelle in The Early Days : A Logical Framework (2019) (0)
- 8. More about Types (2002) (0)
- Mini ML (2004) (0)
- Preface (2008) (0)
- Hotel Key Card System (2006) (0)
- Special Issue on Formal Modeling and Verification of Critical Systems (2008) (0)
- Acknowledgement to referees (2004) (0)
- Type Reconstruction for Type Classes 1 (0)
- TAP 2009: Short papers (2009) (0)
- Semantics of Programming Languages Exercise Sheet 8 Exercise 8 . 1 Definite Initialization Analysis (2012) (0)
- 10. Case Study: Verifying a Security Protocol (2002) (0)
- Closest Pair of Points Algorithms (2020) (0)
- hosted at the Radboud Repository of the (2018) (0)
- Interaction versus Automation: The two Faces of Deduction, 04.10. - 09.10.2009 (2009) (0)
- Preface (2000) (0)
- Gröbner Bases and Buchberger's Algorithm (1998) (0)
- Quantifier Elimination for Linear Arithmetic (2008) (0)
- Dynamic Tables (2015) (0)
- Proof Pearl: Regular Expression Equivalence and Relation Algebra (2011) (0)
- Majority Vote Algorithm Revisited Again (2011) (0)
- Term Rewriting and All That : Combination Problems (1998) (0)
- 2. Functional Programming in HOL (2002) (0)
- Isa be lle β α Isar The Isabelle / Isar Reference Manual (1999) (0)
- Proo f Term s for Simply Type d Highe r Orde r Logic (2000) (0)
- COMPASS WG 6112 Interim Report: October 1, 1992 - September 30, 1993 (1993) (0)
- Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006) (2007) (0)
- Proceedings of the 9th International Conference on Rewriting Techniques and Applications (1998) (0)
- Rewriting Techniques and Applications (1998) (0)
- Isar: a Language for Structured Proofs (2014) (0)
- Sutcliffe 7 . 1 CVC 4 0 . 0 (2012) (0)
- Proceedings of the 14th international conference on Formal Methods (2006) (0)
- Term Rewriting and All That : Completion (1998) (0)
- Logic and Proof Beyond Equality (2014) (0)
- A Verified Implementation of B+-Trees in Isabelle/HOL (2022) (0)
- Case Study: IMP Expressions (2014) (0)
- The Isabelle Cookbook A Gentle Tutorial for Programming on the ML-Level of Isabelle (draft) (2013) (0)
- Preface (2006) (0)
- Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic (2007) (0)
- Term Rewriting and All That : Abstract Reduction Systems (1998) (0)
- 09411 Abstracts Collection - Interaction versus Automation: The two Faces of Deduction (2009) (0)
- 4. Presenting Theories (2002) (0)
- A Formalization and Proof Checker for Isabelle’s Metalogic (2022) (0)
- 3. More Functional Programming (2002) (0)
- 9. Advanced Simplification, Recursion, and Induction (2002) (0)
- 09411 Executive Summary - Interaction versus Automation: The two Faces of Deductions (2009) (0)
- Real-Time Double-Ended Queue (2022) (0)
- Veriied Lexical Analysis (1998) (0)
- A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions (2013) (0)
- Deduction and Arithmetic (Dagstuhl Seminar 13411) (2013) (0)
This paper list is powered by the following services:
Other Resources About Tobias Nipkow
What Schools Are Affiliated With Tobias Nipkow?
Tobias Nipkow is affiliated with the following schools:
