Tobias Nipkow

According to our database1, Tobias Nipkow
  • authored at least 166 papers between 1983 and 2017.
  • has a "Dijkstra number"2 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2017
A Verified Compiler for Probability Density Functions.
CoRR, 2017

Root-Balanced Tree.
Archive of Formal Proofs, 2017

Propositional Proof Systems.
Archive of Formal Proofs, 2017

Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL.
Proceedings of the Integrated Formal Methods - 13th International Conference, 2017

Verified Root-Balanced Trees.
Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

2016
Abstract Interpretation of Annotated Commands.
Archive of Formal Proofs, 2016

Analysis of List Update Algorithms.
Archive of Formal Proofs, 2016

Pairing Heap.
Archive of Formal Proofs, 2016

Verified Analysis of Functional Data Structures.
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

Automatic Functional Correctness Proofs for Functional Search Trees.
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Verified Analysis of List Update Algorithms.
Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

2015
Verified decision procedures for MSO on words based on derivatives of regular expressions.
J. Funct. Program., 2015

A formal proof of the Kepler conjecture.
CoRR, 2015

Parameterized Dynamic Tables.
Archive of Formal Proofs, 2015

Trie.
Archive of Formal Proofs, 2015

Mining the Archive of Formal Proofs.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Amortized Complexity Verified.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

A Verified Compiler for Probability Density Functions.
Proceedings of the Programming Languages and Systems, 2015

2014
Applications of Interactive Proof to Data Flow Analysis and Security.
Proceedings of the Software Systems Safety, 2014

Making security type systems less ad hoc.
it - Information Technology, 2014

Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions.
Archive of Formal Proofs, 2014

Unified Decision Procedures for Regular Expression Equivalence.
Archive of Formal Proofs, 2014

Priority Queues Based on Braun Trees.
Archive of Formal Proofs, 2014

Skew Heap.
Archive of Formal Proofs, 2014

Splay Tree.
Archive of Formal Proofs, 2014

Amortized Complexity Verified.
Archive of Formal Proofs, 2014

Boolean Expression Checkers.
Archive of Formal Proofs, 2014

A Fully Verified Executable LTL Model Checker.
Archive of Formal Proofs, 2014

A Verified Compiler for Probability Density Functions.
Archive of Formal Proofs, 2014

Unified Decision Procedures for Regular Expression Equivalence.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Experience report: the next 1100 Haskell programmers.
Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, 2014

Concrete Semantics - With Isabelle/HOL
Springer, ISBN: 978-3-319-10542-0, 2014

2013
Formal Verification of Language-Based Concurrent Noninterference.
J. Formalized Reasoning, 2013

Deduction and Arithmetic (Dagstuhl Seminar 13411).
Dagstuhl Reports, 2013

A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

Data Refinement in Isabelle/HOL.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Verified decision procedures for MSO on words based on derivatives of regular expressions.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

Formalizing Probabilistic Noninterference.
Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

A Fully Verified Executable LTL Model Checker.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference.
Proceedings of the Algebra and Coalgebra in Computer Science, 2013

2012
Interactive Proof: Introduction to Isabelle/HOL.
Proceedings of the Software Safety and Security - Tools for Analysis and Verification, 2012

A compiled implementation of normalisation by evaluation.
J. Funct. Program., 2012

Proof Pearl: Regular Expression Equivalence and Relation Algebra.
J. Autom. Reasoning, 2012

Interactive verification of Markov chains: Two distributed protocol case studies
Proceedings of the Proceedings Quantities in Formal Methods, 2012

Markov Models.
Archive of Formal Proofs, 2012

Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Verifying pCTL Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Abstract Interpretation of Annotated Commands.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Proving Concurrent Noninterference.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011
Majority Vote Algorithm Revisited Again.
Int. J. Software and Informatics, 2011

Gauss-Jordan Elimination for Matrices Represented as Functions.
Archive of Formal Proofs, 2011

Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism.
Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Automatic Proof and Disproof in Isabelle/HOL.
Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

Proof Pearl: The Marriage Theorem.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011

Extending Hindley-Milner Type Inference with Coercive Structural Subtyping.
Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010
Linear Quantifier Elimination.
J. Autom. Reasoning, 2010

Deduktion: von der Theorie zur Anwendung.
Informatik Spektrum, 2010

A Revision of the Proof of the Kepler Conjecture.
Discrete & Computational Geometry, 2010

List Index.
Archive of Formal Proofs, 2010

Regular Sets and Expressions.
Archive of Formal Proofs, 2010

Hall's Marriage Theorem.
Archive of Formal Proofs, 2010

Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Code Generation via Higher-Order Rewrite Systems.
Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010

Sledgehammer: Judgement Day.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009
Social Choice Theory in HOL.
J. Autom. Reasoning, 2009

Flyspeck II: the basic linear programs.
Ann. Math. Artif. Intell., 2009

09411 Executive Summary - Interaction versus Automation: The two Faces of Deductions.
Proceedings of the Interaction versus Automation: The two Faces of Deduction, 04.10., 2009

09411 Abstracts Collection - Interaction versus Automation: The two Faces of Deduction.
Proceedings of the Interaction versus Automation: The two Faces of Deduction, 04.10., 2009

2008
Proof Synthesis and Reflection for Linear Arithmetic.
J. Autom. Reasoning, 2008

Preface.
J. Autom. Reasoning, 2008

Fun With Tilings.
Archive of Formal Proofs, 2008

Arrow and Gibbard-Satterthwaite.
Archive of Formal Proofs, 2008

Fun With Functions.
Archive of Formal Proofs, 2008

Quantifier Elimination for Linear Arithmetic.
Archive of Formal Proofs, 2008

Normalization by Evaluation.
Archive of Formal Proofs, 2008

The Isabelle Framework.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

A Compiled Implementation of Normalization by Evaluation.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Linear Quantifier Elimination.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
Preface.
Electr. Notes Theor. Comput. Sci., 2007

Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

C++ ist typsicher? Garantiert!
Proceedings of the Software Engineering 2007, 2007

Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic.
Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

2006
A machine-checked model for a Java-like language, virtual machine, and compiler.
ACM Trans. Program. Lang. Syst., 2006

Hotel Key Card System.
Archive of Formal Proofs, 2006

Abstract Hoare Logics.
Archive of Formal Proofs, 2006

Flyspeck I: Tame Graphs.
Archive of Formal Proofs, 2006

An operational semantics and type safety prooffor multiple inheritance in C++.
Proceedings of the 21th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2006

Verifying a Hotel Key Card System.
Proceedings of the Theoretical Aspects of Computing, 2006

Flyspeck I: Tame Graphs.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005
Proving pointer programs in higher-order logic.
Inf. Comput., 2005

Bytecode Analysis for Proof Carrying Code.
Electr. Notes Theor. Comput. Sci., 2005

Jinja is not Java.
Archive of Formal Proofs, 2005

Proof Pearl: Defining Functions over Finite Sets.
Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic.
Proceedings of the Logic for Programming, 2005

Asserting Bytecode Safety.
Proceedings of the Programming Languages and Systems, 2005

Towards a Verified Enumeration of All Tame Plane Graphs.
Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

2004
AVL Trees.
Archive of Formal Proofs, 2004

Compiling Exceptions Correctly.
Archive of Formal Proofs, 2004

Functional Automata.
Archive of Formal Proofs, 2004

Mini ML.
Archive of Formal Proofs, 2004

Certifying Machine Code Safety: Shallow Versus Deep Embedding.
Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Random Testing in Isabelle/HOL.
Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

Prototyping Proof Carrying Code.
Proceedings of the Exploring New Frontiers of Theoretical Informatics, 2004

2003
Verified bytecode verifiers.
Theor. Comput. Sci., 2003

Java Bytecode Verification.
J. Autom. Reasoning, 2003

Proving Pointer Programs in Higher-Order Logic.
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002
Structured Proofs in Isar/HOL.
Proceedings of the Types for Proofs and Programs, Second International Workshop, 2002

The 5 Colour Theorem in Isabelle/Isar.
Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited.
Proceedings of the FME 2002: Formal Methods, 2002

Hoare Logics for Recursive Procedures and Unbounded Nondeterminism.
Proceedings of the Computer Science Logic, 16th International Workshop, 2002

Isabelle/HOL - A Proof Assistant for Higher-Order Logic
Lecture Notes in Computer Science 2283, Springer, ISBN: 3-540-43376-7, 2002

2001
More Church-Rosser Proofs.
J. Autom. Reasoning, 2001

Verified lightweight bytecode verification.
Concurrency and Computation: Practice and Experience, 2001

Verified Bytecode Verifiers.
Proceedings of the Foundations of Software Science and Computation Structures, 2001

2000
Preface.
Inf. Comput., 2000

Executing Higher Order Logic.
Proceedings of the Types for Proofs and Programs, International Workshop, 2000

Proof Terms for Simply Typed Higher Order Logic.
Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

1999
HOLCF=HOL+LCF.
J. Funct. Program., 1999

Type Inference Verified: Algorithm W in Isabelle/HOL.
J. Autom. Reasoning, 1999

Machine-Checking the Java Specification: Proving Type-Safety.
Proceedings of the Formal Syntax and Semantics of Java, 1999

Owicki/Gries in Isabelle/HOL.
Proceedings of the Fundamental Approaches to Software Engineering, 1999

Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract).
Proceedings of the Automated Deduction, 1999

1998
Higher-Order Rewrite Systems and Their Confluence.
Theor. Comput. Sci., 1998

Winskel is (almost) Right: Towards a Mechanized Semantics.
Formal Asp. Comput., 1998

Verified Lexical Analysis.
Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998

Javalight is Type-Safe - Definitely.
Proceedings of the POPL '98, 1998

Term rewriting and all that.
Cambridge University Press, ISBN: 978-0-521-45520-6, 1998

1997
Traces of I/O-Automata in Isabelle/HOLCF.
Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

1996
Type Inference Verified: Algorithm W in Isabelle/HOL.
Proceedings of the Types for Proofs and Programs, 1996

Formal Verification of Algorithm W: The Monomorphic Case.
Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996

Winskel is (Almost) Right: Towards a Mechanized Semantics Textbook.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1996

More Church-Rosser Proofs (in Isabelle/HOL).
Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995
Type Reconstruction for Type Classes.
J. Funct. Program., 1995

Combining Model Checking and Deduction for I/O-Automata.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1995

Higher-Order Rewrite Systems (Abstract).
Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995

1994
Reduction and Unification in Lambda Calculi with a General Notion of Subtype.
J. Autom. Reasoning, 1994

I/Q Automata in Isabelle/HOL.
Proceedings of the Types for Proofs and Programs, 1994

Interpreter Verification for a Functional Language.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1994

1993
Orthogonal Higher-Order Rewrite Systems are Confluent.
Proceedings of the Typed Lambda Calculi and Applications, 1993

Type Checking Type Classes.
Proceedings of the Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993

Functional Unification of Higher-Order Patterns
Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

1992
Reduction and Unification in Lambda Calculi with Subtypes.
Proceedings of the Automated Deduction, 1992

Isabelle-91.
Proceedings of the Automated Deduction, 1992

1991
Combining Matching Algorithms: The Regular Case.
J. Symb. Comput., 1991

Constructive Rewriting.
Comput. J., 1991

Modular Higher-Order E-Unification.
Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

Higher-Order Critical Pairs
Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

Type Classes and Overloading Resolution via Order-Sorted Unification.
Proceedings of the Functional Programming Languages and Computer Architecture, 1991

1990
Unification in Primal Algebras, Their Powers and Their Varieties
J. ACM, October, 1990

Proof Transformations for Equational Theories
Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

Higher-Order Unification, Polymorphism, and Subsorts (Extended Abstract).
Proceedings of the Conditional and Typed Rewriting Systems, 1990

Ordered Rewriting and Confluence.
Proceedings of the 10th International Conference on Automated Deduction, 1990

1989
Equational Reasoning in Isabelle.
Sci. Comput. Program., 1989

Boolean Unification - The Story So Far.
J. Symb. Comput., 1989

Term Rewriting and Beyond - Theorem Proving in Isabelle.
Formal Asp. Comput., 1989

Combining Matching Algorithms: The Rectangular Case.
Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

Formal Verification of Data Type Refinement - Theory and Practice.
Proceedings of the Stepwise Refinement of Distributed Systems, 1989

1988
Unification in Boolean Rings.
J. Autom. Reasoning, 1988

Unification in Primal Algebras.
Proceedings of the CAAP '88, 1988

1987
Are Homomorphisms Sufficient for Behavioural Implementations of Deterministic and Nondeterministic Data Types?
Proceedings of the STACS 87, 1987

Observing Non-Deterministic Data Types.
Proceedings of the Recent Trends in Data Type Specification, 1987

1986
Behavioural implementation concepts for nondeterministic data types.
PhD thesis, 1986

Non-deterministic Data Types: Models and Implementations.
Acta Inf., 1986

Unification in Boolean Rings.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

Behavioural Implementations of Non-Deterministic Data Types.
ADT, 1986

1983
A decidability result about sufficient-completeness of axiomatically specified abstract data types.
Proceedings of the Theoretical Computer Science, 1983


  Loading...