9 citations · 22 across the 10 of their papers we have counts for
11 papers
Verification of NP-hardness Reduction Functions for Exact Lattice Problems
Katharina Kreuzer, Tobias Nipkow
This paper describes the formal verification of NP-hardness reduction functions of two key problems relevant in algebraic lattice theory: the closest vector problem and the shortes…
A Verified Implementation of B+-Trees in Isabelle/HOL
Niels Mündler, Tobias Nipkow
In this paper we present the verification of an imperative implementation of the ubiquitous B+-tree data structure in the interactive theorem prover Isabelle/HOL. The implementatio…
Isabelle's Metalogic: Formalization and Proof Checker
Tobias Nipkow, Simon Roßkopf
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogi…
Verified Approximation Algorithms
Robin Eßmann, Tobias Nipkow, Simon Robillard +1
We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, set cover, center selection, load balanci…
A Verified Decision Procedure for Orders in Isabelle/HOL
Lukas Stevens, Tobias Nipkow
We present the first verified implementation of a decision procedure for the quantifier-free theory of partial and linear orders. We formalise the procedure in Isabelle/HOL and pro…
From LCF to Isabelle/HOL
Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel
Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its di…