Tobias Nipkow
2021
Isabelle's Metalogic: Formalization and Proof Checker
by Tobias Nipkow and Simon Roßkopf
2020
Verified Approximation Algorithms
by Robin Eßmann, Tobias Nipkow, Simon Robillard and Ujkan Sulejmani
Closest Pair of Points Algorithms
by Martin Rau and Tobias Nipkow
2019
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
by Peter Lammich and Tobias Nipkow
2018
Optimal Binary Search Trees
by Tobias Nipkow and Dániel Somogyi
Monadification, Memoization and Dynamic Programming
by Simon Wimmer, Shuwei Hu and Tobias Nipkow
Hoare Logics for Time Bounds
by Maximilian P. L. Haslbeck and Tobias Nipkow
Treaps
by Maximilian P. L. Haslbeck, Manuel Eberl and Tobias Nipkow
2017
Propositional Proof Systems
by Julius Michaelis and Tobias Nipkow
2016
Abstract Interpretation of Annotated Commands
by Tobias Nipkow
Analysis of List Update Algorithms
by Maximilian P. L. Haslbeck and Tobias Nipkow
2015
2014
A Verified Compiler for Probability Density Functions
by Manuel Eberl, Johannes Hölzl and Tobias Nipkow
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
by Dmitriy Traytel and Tobias Nipkow
A Fully Verified Executable LTL Model Checker
by Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf and Jan-Georg Smaus
Unified Decision Procedures for Regular Expression Equivalence
by Tobias Nipkow and Dmitriy Traytel
2012
2011
Gauss-Jordan Elimination for Matrices Represented as Functions
by Tobias Nipkow
2010
Regular Sets and Expressions
by Alexander Krauss and Tobias Nipkow
2008
Normalization by Evaluation
by Klaus Aehlig and Tobias Nipkow
Quantifier Elimination for Linear Arithmetic
by Tobias Nipkow