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