ⅢPROOFS ABOUT FUNDAMENTAL DATATYPES 7 Organizing Theory Development With Athena Modules 8 Natural Number Orderings 9 Integer Representations and Proof Mappings 10 Fundamental Discrete Structures
ⅣPROOF ABOUT ALGORITHMS 11 A Binary Search Algorithm 12 A Fast Exponentiation Algorithm 13 Euclid's Algorithm for Greatest Common Division
ⅤPROOFS AT AN ABSTRACT LEVEL 14 Abstract Stuctures 15 Abstract Algorithms 16 Algorithms on Memory Abstractons
ⅥPROOFS ABOUT PROGRAMMING LANGUAGES 17 A Correctness Proof for a Toy Compiler 18 A Simple Imperative Programming Language A Athena Reference B Logic Programming and Prolog