dblp.uni-trier.dewww.uni-trier.de

Tobias Nipkow Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo
Home Page

*2009
89EEStefan 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 Springer 2009
2008
88EETobias Nipkow: Linear Quantifier Elimination. IJCAR 2008: 18-33
87EEMakarius Wenzel, Lawrence C. Paulson, Tobias Nipkow: The Isabelle Framework. TPHOLs 2008: 33-38
86EEKlaus Aehlig, Florian Haftmann, Tobias Nipkow: A Compiled Implementation of Normalization by Evaluation. TPHOLs 2008: 39-54
85EEAmine Chaieb, Tobias Nipkow: Proof Synthesis and Reflection for Linear Arithmetic. J. Autom. Reasoning 41(1): 33-59 (2008)
84EESerge 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
82EELukas Bulwahn, Alexander Krauss, Tobias Nipkow: Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. TPHOLs 2007: 38-53
81EETobias Nipkow: Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic. VERIFY 2007
80EEStephan 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
78EETobias Nipkow: Verifying a Hotel Key Card System. ICTAC 2006: 1-14
77EETobias Nipkow, Gertrud Bauer, Paula Schultz: Flyspeck I: Tame Graphs. IJCAR 2006: 21-35
76EEDaniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip: An operational semantics and type safety prooffor multiple inheritance in C++. OOPSLA 2006: 345-362
75EEGerwin 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
74EEMartin Wildmoser, Tobias Nipkow: Asserting Bytecode Safety. ESOP 2005: 326-341
73EEAmine Chaieb, Tobias Nipkow: Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. LPAR 2005: 367-380
72EETobias Nipkow, Gertrud Bauer: Towards a Verified Enumeration of All Tame Plane Graphs. Mathematics, Algorithms, Proofs 2005
71EETobias Nipkow, Lawrence C. Paulson: Proof Pearl: Defining Functions over Finite Sets. TPHOLs 2005: 385-396
70EEMartin Wildmoser, Amine Chaieb, Tobias Nipkow: Bytecode Analysis for Proof Carrying Code. Electr. Notes Theor. Comput. Sci. 141(1): 19-34 (2005)
69EEFarhad 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
67EEStefan Berghofer, Tobias Nipkow: Random Testing in Isabelle/HOL. SEFM 2004: 230-239
66EEMartin Wildmoser, Tobias Nipkow: Certifying Machine Code Safety: Shallow Versus Deep Embedding. TPHOLs 2004: 305-320
2003
65EEFarhad Mehta, Tobias Nipkow: Proving Pointer Programs in Higher-Order Logic. CADE 2003: 121-135
64EETobias Nipkow: Java Bytecode Verification. J. Autom. Reasoning 30(3-4): 233-233 (2003)
63EEGerwin 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
61EETobias Nipkow: Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. CSL 2002: 103-119
60EEDavid von Oheimb, Tobias Nipkow: Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. FME 2002: 89-105
59EEGertrud Bauer, Tobias Nipkow: The 5 Colour Theorem in Isabelle/Isar. TPHOLs 2002: 67-82
58EETobias 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
56EETobias 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
53EEStefan Berghofer, Tobias Nipkow: Proof Terms for Simply Typed Higher Order Logic. TPHOLs 2000: 38-52
52EEStefan Berghofer, Tobias Nipkow: Executing Higher Order Logic. TYPES 2000: 24-40
51 Tobias Nipkow: Preface. Inf. Comput. 159(1-2): 1 (2000)
1999
50EETobias 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
48EEDavid 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
44EETobias Nipkow, David von Oheimb: Javalight is Type-Safe - Definitely. POPL 1998: 161-170
43EETobias 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)
41EERichard Mayr, Tobias Nipkow: Higher-Order Rewrite Systems and Their Confluence. Theor. Comput. Sci. 192(1): 3-29 (1998)
1997
40EEOlaf Müller, Tobias Nipkow: Traces of I/O-Automata in Isabelle/HOLCF. TAPSOFT 1997: 580-594
1996
39EETobias Nipkow: More Church-Rosser Proofs (in Isabelle/HOL). CADE 1996: 733-747
38EETobias Nipkow: Winskel is (Almost) Right: Towards a Mechanized Semantics Textbook. FSTTCS 1996: 180-192
37EEDieter 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
35EETobias 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
30EEManfred 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
24EETobias Nipkow, Zhenyu Qian: Reduction and Unification in Lambda Calculi with Subtypes. CADE 1992: 66-78
23EETobias 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
20EETobias 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
17EEUrsula 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
14EETobias Nipkow: Unification in Primal Algebras, Their Powers and Their Varieties J. ACM 37(4): 742-776 (1990)
1989
13EETobias Nipkow: Formal Verification of Data Type Refinement - Theory and Practice. REX Workshop 1989: 561-591
12EETobias 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
8EETobias 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
5EETobias 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
3EEUrsula 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

Coauthor Index

1Klaus Aehlig [86]
2Serge Autexier [84]
3Hendrik Pieter Barendregt (Henk Barendregt) [32]
4Gertrud Bauer [59] [72] [77]
5Stefan Berghofer [52] [53] [67] [89]
6Manfred Broy [30]
7Lukas Bulwahn [82]
8Amine Chaieb [70] [73] [85]
9Rajeev Goré [57]
10Florian Haftmann [86]
11Jan Heering [31]
12Ursula Hinkel [30]
13Gerwin Klein [55] [63] [68] [75]
14Alexander Krauss [82]
15Alexander Leitsch [57]
16Heiko Mantel [84]
17Ursula Martin [3] [7] [10] [17]
18Richard Mayr [41]
19Farhad Mehta [65] [69]
20Karl Meinke [31]
21Stephan Merz [80] [84]
22Jayadev Misra [79]
23Bernhard Möller [31]
24Olaf Müller [34] [40] [46]
25Sebastian Nanz [68]
26Wolfgang Naraschewski [36] [47]
27Dieter Nazareth [37]
28Leonor Prensa Nieto [49]
29David von Oheimb [44] [46] [48] [60]
30Lawrence C. Paulson [23] [62] [71] [87]
31Christian Prehofer [26] [30] [33]
32Zhenyu Qian [20] [24] [28]
33Birgit Schieder [30]
34Paula Schultz [77]
35Emil Sekerinski [79]
36Konrad Slind [29]
37Oscar Slotosch [46]
38Gregor Snelting [22] [76] [83]
39Frank Tip [76] [83]
40Christian Urban [89]
41Daniel Wasserrab [76] [83]
42Gerhard Weikum [1]
43Markus Wenzel (Makarius Wenzel) [62] [87] [89]
44Martin Wildmoser [66] [68] [70] [74]

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)