The SCEAS System
Navigation Menu
Introduction
Collection Based
Clustering
Ranking
Paper Based
Journals
Conferences
DB Status
Statistics
Search

Search the dblp DataBase

Title:
Author:
Tobias Nipkow: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. Tobias Nipkow, Christian Prehofer
    Type Checking Type Classes. [Citation Graph (1, 0)][DBLP]
    POPL, 1993, pp:409-418 [Conf]
  2. Ursula Martin, Tobias Nipkow
    Unification in Boolean Rings. [Citation Graph (1, 0)][DBLP]
    J. Autom. Reasoning, 1988, v:4, n:4, pp:381-396 [Journal]
  3. Tobias Nipkow
    Behavioural Implementations of Non-Deterministic Data Types. [Citation Graph (0, 0)][DBLP]
    ADT, 1986, pp:- [Conf]
  4. Tobias Nipkow
    Observing Non-Deterministic Data Types. [Citation Graph (0, 0)][DBLP]
    ADT, 1987, pp:170-183 [Conf]
  5. Tobias Nipkow
    Unification in Primal Algebras. [Citation Graph (0, 0)][DBLP]
    CAAP, 1988, pp:117-131 [Conf]
  6. Ursula Martin, Tobias Nipkow
    Unification in Boolean Rings. [Citation Graph (0, 0)][DBLP]
    CADE, 1986, pp:506-513 [Conf]
  7. Ursula Martin, Tobias Nipkow
    Ordered Rewriting and Confluence. [Citation Graph (0, 0)][DBLP]
    CADE, 1990, pp:366-380 [Conf]
  8. Farhad Mehta, Tobias Nipkow
    Proving Pointer Programs in Higher-Order Logic. [Citation Graph (0, 0)][DBLP]
    CADE, 2003, pp:121-135 [Conf]
  9. Tobias Nipkow
    More Church-Rosser Proofs (in Isabelle/HOL). [Citation Graph (0, 0)][DBLP]
    CADE, 1996, pp:733-747 [Conf]
  10. Tobias Nipkow
    Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract). [Citation Graph (0, 0)][DBLP]
    CADE, 1999, pp:398- [Conf]
  11. Tobias Nipkow, Gertrud Bauer, Paula Schultz
    Flyspeck I: Tame Graphs. [Citation Graph (0, 0)][DBLP]
    IJCAR, 2006, pp:21-35 [Conf]
  12. Tobias Nipkow, Lawrence C. Paulson
    Isabelle-91. [Citation Graph (0, 0)][DBLP]
    CADE, 1992, pp:673-676 [Conf]
  13. Tobias Nipkow, Zhenyu Qian
    Reduction and Unification in Lambda Calculi with Subtypes. [Citation Graph (0, 0)][DBLP]
    CADE, 1992, pp:66-78 [Conf]
  14. Tobias Nipkow
    Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. [Citation Graph (0, 0)][DBLP]
    CSL, 2002, pp:103-119 [Conf]
  15. Tobias Nipkow
    Higher-Order Unification, Polymorphism, and Subsorts (Extended Abstract). [Citation Graph (0, 0)][DBLP]
    CTRS, 1990, pp:436-447 [Conf]
  16. Tobias Nipkow, Gertrud Bauer
    Towards a Verified Enumeration of All Tame Plane Graphs. [Citation Graph (0, 0)][DBLP]
    Mathematics, Algorithms, Proofs, 2005, pp:- [Conf]
  17. Martin Wildmoser, Tobias Nipkow
    Asserting Bytecode Safety. [Citation Graph (0, 0)][DBLP]
    ESOP, 2005, pp:326-341 [Conf]
  18. Tobias Nipkow, Leonor Prensa Nieto
    Owicki/Gries in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    FASE, 1999, pp:188-203 [Conf]
  19. David von Oheimb, Tobias Nipkow
    Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. [Citation Graph (0, 0)][DBLP]
    FME, 2002, pp:89-105 [Conf]
  20. Tobias Nipkow
    Verified Bytecode Verifiers. [Citation Graph (0, 0)][DBLP]
    FoSSaCS, 2001, pp:347-363 [Conf]
  21. Tobias Nipkow, Gregor Snelting
    Type Classes and Overloading Resolution via Order-Sorted Unification. [Citation Graph (0, 0)][DBLP]
    FPCA, 1991, pp:1-14 [Conf]
  22. Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, Birgit Schieder
    Interpreter Verification for a Functional Language. [Citation Graph (0, 0)][DBLP]
    FSTTCS, 1994, pp:77-88 [Conf]
  23. Tobias Nipkow
    Winskel is (Almost) Right: Towards a Mechanized Semantics Textbook. [Citation Graph (0, 0)][DBLP]
    FSTTCS, 1996, pp:180-192 [Conf]
  24. Tobias Nipkow
    Verifying a Hotel Key Card System. [Citation Graph (0, 0)][DBLP]
    ICTAC, 2006, pp:1-14 [Conf]
  25. Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz
    Prototyping Proof Carrying Code. [Citation Graph (0, 0)][DBLP]
    IFIP TCS, 2004, pp:333-348 [Conf]
  26. David von Oheimb, Tobias Nipkow
    Machine-Checking the Java Specification: Proving Type-Safety. [Citation Graph (0, 0)][DBLP]
    Formal Syntax and Semantics of Java, 1999, pp:119-156 [Conf]
  27. Tobias Nipkow
    Proof Transformations for Equational Theories [Citation Graph (0, 0)][DBLP]
    LICS, 1990, pp:278-288 [Conf]
  28. Tobias Nipkow
    Higher-Order Critical Pairs [Citation Graph (0, 0)][DBLP]
    LICS, 1991, pp:342-349 [Conf]
  29. Tobias Nipkow
    Functional Unification of Higher-Order Patterns [Citation Graph (0, 0)][DBLP]
    LICS, 1993, pp:64-74 [Conf]
  30. Amine Chaieb, Tobias Nipkow
    Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. [Citation Graph (0, 0)][DBLP]
    LPAR, 2005, pp:367-380 [Conf]
  31. Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip
    An operational semantics and type safety prooffor multiple inheritance in C++. [Citation Graph (0, 0)][DBLP]
    OOPSLA, 2006, pp:345-362 [Conf]
  32. Tobias Nipkow, David von Oheimb
    Javalight is Type-Safe - Definitely. [Citation Graph (0, 0)][DBLP]
    POPL, 1998, pp:161-170 [Conf]
  33. Tobias Nipkow
    Formal Verification of Data Type Refinement - Theory and Practice. [Citation Graph (0, 0)][DBLP]
    REX Workshop, 1989, pp:561-591 [Conf]
  34. Tobias Nipkow
    Combining Matching Algorithms: The Rectangular Case. [Citation Graph (0, 0)][DBLP]
    RTA, 1989, pp:343-358 [Conf]
  35. Tobias Nipkow
    Higher-Order Rewrite Systems (Abstract). [Citation Graph (0, 0)][DBLP]
    RTA, 1995, pp:256- [Conf]
  36. Tobias Nipkow, Zhenyu Qian
    Modular Higher-Order E-Unification. [Citation Graph (0, 0)][DBLP]
    RTA, 1991, pp:200-214 [Conf]
  37. Stefan Berghofer, Tobias Nipkow
    Random Testing in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    SEFM, 2004, pp:230-239 [Conf]
  38. Tobias Nipkow
    Are Homomorphisms Sufficient for Behavioural Implementations of Deterministic and Nondeterministic Data Types? [Citation Graph (0, 0)][DBLP]
    STACS, 1987, pp:260-271 [Conf]
  39. Olaf Müller, Tobias Nipkow
    Combining Model Checking and Deduction for I/O-Automata. [Citation Graph (0, 0)][DBLP]
    TACAS, 1995, pp:1-16 [Conf]
  40. Olaf Müller, Tobias Nipkow
    Traces of I/O-Automata in Isabelle/HOLCF. [Citation Graph (0, 0)][DBLP]
    TAPSOFT, 1997, pp:580-594 [Conf]
  41. Tobias Nipkow, Gerhard Weikum
    A decidability result about sufficient-completeness of axiomatically specified abstract data types. [Citation Graph (0, 0)][DBLP]
    Theoretical Computer Science, 1983, pp:257-268 [Conf]
  42. Tobias Nipkow
    Orthogonal Higher-Order Rewrite Systems are Confluent. [Citation Graph (0, 0)][DBLP]
    TLCA, 1993, pp:306-317 [Conf]
  43. Gertrud Bauer, Tobias Nipkow
    The 5 Colour Theorem in Isabelle/Isar. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2002, pp:67-82 [Conf]
  44. Stefan Berghofer, Tobias Nipkow
    Proof Terms for Simply Typed Higher Order Logic. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:38-52 [Conf]
  45. Dieter Nazareth, Tobias Nipkow
    Formal Verification of Algorithm W: The Monomorphic Case. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1996, pp:331-345 [Conf]
  46. Tobias Nipkow
    Verified Lexical Analysis. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1998, pp:1-15 [Conf]
  47. Tobias Nipkow, Lawrence C. Paulson
    Proof Pearl: Defining Functions over Finite Sets. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2005, pp:385-396 [Conf]
  48. Martin Wildmoser, Tobias Nipkow
    Certifying Machine Code Safety: Shallow Versus Deep Embedding. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2004, pp:305-320 [Conf]
  49. Tobias Nipkow
    Structured Proofs in Isar/HOL. [Citation Graph (0, 0)][DBLP]
    TYPES, 2002, pp:259-278 [Conf]
  50. Tobias Nipkow, Konrad Slind
    I/Q Automata in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    TYPES, 1994, pp:101-119 [Conf]
  51. Stefan Berghofer, Tobias Nipkow
    Executing Higher Order Logic. [Citation Graph (0, 0)][DBLP]
    TYPES, 2000, pp:24-40 [Conf]
  52. Wolfgang Naraschewski, Tobias Nipkow
    Type Inference Verified: Algorithm W in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    TYPES, 1996, pp:317-332 [Conf]
  53. Tobias Nipkow
    Non-deterministic Data Types: Models and Implementations. [Citation Graph (0, 0)][DBLP]
    Acta Inf., 1986, v:22, n:6, pp:629-661 [Journal]
  54. Tobias Nipkow
    Constructive Rewriting. [Citation Graph (0, 0)][DBLP]
    Comput. J., 1991, v:34, n:1, pp:34-41 [Journal]
  55. Gerwin Klein, Tobias Nipkow
    Verified lightweight bytecode verification. [Citation Graph (0, 0)][DBLP]
    Concurrency and Computation: Practice and Experience, 2001, v:13, n:13, pp:1133-1151 [Journal]
  56. Martin Wildmoser, Amine Chaieb, Tobias Nipkow
    Bytecode Analysis for Proof Carrying Code. [Citation Graph (0, 0)][DBLP]
    Electr. Notes Theor. Comput. Sci., 2005, v:141, n:1, pp:19-34 [Journal]
  57. Tobias Nipkow
    Term Rewriting and Beyond - Theorem Proving in Isabelle. [Citation Graph (0, 0)][DBLP]
    Formal Asp. Comput., 1989, v:1, n:4, pp:320-338 [Journal]
  58. Tobias Nipkow
    Winskel is (almost) Right: Towards a Mechanized Semantics. [Citation Graph (0, 0)][DBLP]
    Formal Asp. Comput., 1998, v:10, n:2, pp:171-186 [Journal]
  59. Farhad Mehta, Tobias Nipkow
    Proving pointer programs in higher-order logic. [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 2005, v:199, n:1-2, pp:200-227 [Journal]
  60. Tobias Nipkow
    Preface. [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 2000, v:159, n:1-2, pp:1- [Journal]
  61. Tobias Nipkow
    Unification in Primal Algebras, Their Powers and Their Varieties [Citation Graph (0, 0)][DBLP]
    J. ACM, 1990, v:37, n:4, pp:742-776 [Journal]
  62. Wolfgang Naraschewski, Tobias Nipkow
    Type Inference Verified: Algorithm W in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 1999, v:23, n:3-4, pp:299-318 [Journal]
  63. Tobias Nipkow
    More Church-Rosser Proofs. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 2001, v:26, n:1, pp:51-66 [Journal]
  64. Tobias Nipkow
    Java Bytecode Verification. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 2003, v:30, n:3-4, pp:233-233 [Journal]
  65. Zhenyu Qian, Tobias Nipkow
    Reduction and Unification in Lambda Calculi with a General Notion of Subtype. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 1994, v:12, n:3, pp:389-406 [Journal]
  66. Olaf Müller, Tobias Nipkow, David von Oheimb, Oscar Slotosch
    HOLCF=HOL+LCF. [Citation Graph (0, 0)][DBLP]
    J. Funct. Program., 1999, v:9, n:2, pp:191-223 [Journal]
  67. Tobias Nipkow, Christian Prehofer
    Type Reconstruction for Type Classes. [Citation Graph (0, 0)][DBLP]
    J. Funct. Program., 1995, v:5, n:2, pp:201-224 [Journal]
  68. Ursula Martin, Tobias Nipkow
    Boolean Unification - The Story So Far. [Citation Graph (0, 0)][DBLP]
    J. Symb. Comput., 1989, v:7, n:3/4, pp:275-293 [Journal]
  69. Tobias Nipkow
    Combining Matching Algorithms: The Regular Case. [Citation Graph (0, 0)][DBLP]
    J. Symb. Comput., 1991, v:12, n:6, pp:633-654 [Journal]
  70. Tobias Nipkow
    Equational Reasoning in Isabelle. [Citation Graph (0, 0)][DBLP]
    Sci. Comput. Program., 1989, v:12, n:2, pp:123-149 [Journal]
  71. Gerwin Klein, Tobias Nipkow
    Verified bytecode verifiers. [Citation Graph (0, 0)][DBLP]
    Theor. Comput. Sci., 2003, v:3, n:298, pp:583-626 [Journal]
  72. Richard Mayr, Tobias Nipkow
    Higher-Order Rewrite Systems and Their Confluence. [Citation Graph (0, 0)][DBLP]
    Theor. Comput. Sci., 1998, v:192, n:1, pp:3-29 [Journal]
  73. Gerwin Klein, Tobias Nipkow
    A machine-checked model for a Java-like language, virtual machine, and compiler. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Program. Lang. Syst., 2006, v:28, n:4, pp:619-695 [Journal]
  74. Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip
    C++ ist typsicher? Garantiert! [Citation Graph (0, 0)][DBLP]
    Software Engineering, 2007, pp:29-34 [Conf]
  75. Lukas Bulwahn, Alexander Krauss, Tobias Nipkow
    Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2007, pp:38-53 [Conf]
  76. Stephan Merz, Tobias Nipkow
    Preface. [Citation Graph (0, 0)][DBLP]
    Electr. Notes Theor. Comput. Sci., 2007, v:185, n:, pp:1-2 [Journal]

  77. Linear Quantifier Elimination. [Citation Graph (, )][DBLP]


  78. Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic. [Citation Graph (, )][DBLP]


  79. Sledgehammer: Judgement Day. [Citation Graph (, )][DBLP]


  80. Code Generation via Higher-Order Rewrite Systems. [Citation Graph (, )][DBLP]


  81. The Isabelle Framework. [Citation Graph (, )][DBLP]


  82. A Compiled Implementation of Normalization by Evaluation. [Citation Graph (, )][DBLP]


  83. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. [Citation Graph (, )][DBLP]


  84. Flyspeck II: the basic linear programs. [Citation Graph (, )][DBLP]


  85. A Revision of the Proof of the Kepler Conjecture. [Citation Graph (, )][DBLP]


Search in 0.004secs, Finished in 0.455secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
Introduction Collection Based Clustering Ranking Paper Based Journals Conferences DB Status Statistics Search
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002