Dictionary Abstractions and Implementations in Isabelle/HOL

Bryan Ford

This directory contains models in Isabelle/HOL of some classic dictionary abstractions and implementation algorithms, which I developed as part of a class project. They may serve as good examples of the use of basic Isabelle facilities such as primitive recursion and inductive proofs.