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.

Contents:

• Project Report: HTML PS
• Presentation Slides: HTML KPresenter
• Isabelle Source:
  • Dictionary Abstraction
    • List Implementation
    • Hash Table Implementation
    • Binary Tree Implementation
  • Undoable Dictionary Abstraction
    • Reverse ChangeLog Implementation