Recent advances in termination analysis have yielded new methods and tools that are highly automatic. However, when they fail, even experts have difficulty understanding why and de...
Lebesgue integration is a fundamental concept in many mathematical theories, such as real analysis, probability and information theory. Reported higher-order-logic formalizations o...
We present a new formalization of the algebraic hierarchy in Coq, exploiting its new type class mechanism to make practical a solution formerly thought infeasible. Our approach add...
The Isabelle Collections Framework (ICF) provides a unified framework for using verified collection data structures in Isabelle/HOL formalizations and generating efficient functi...
Abstract. Rippling is a heuristic used to guide rewriting and is typically used for inductive theorem proving. We introduce a method to support case-analysis within rippling. Like ...
Pitts et al introduced a beautiful theory about names and binding based on the notions of permutation and support. The engineering challenge is to smoothly adapt this theory to a t...