Hand Made Tatami Demos Homepage

---

The proofs linked to this page are "demos" in the sense that they illustrate the functionality of a system that is only partially built. These examples have been hand built to show what it is like to browse tatami proofs, though not what it is like to build them using the Kumo tool. For that, see the Kumo homepage and (to a lesser extent) the Kumo generated demo webpages. These demos assume familiarity with many (order) sorted algebra and with OBJ; without this background, you will not be able to understand the proofs. Suitable material can be found in the following two books:

• Algebraic Semantics of Imperative Programs.
• Theorem Proving and Algebra.

The coinduction proofs will also require familiarity with hidden (order) sorted algebra. See:

• Tutorial material on hidden algebra, induction, first order logic, etc.;
• "A Hidden Agenda" for complete details; and
• "Extended Abstract of a Hidden Agenda" for a brief but precise overview.

---

The following examples are currently available for browsing:

• An inductive proof that 1+...+ n = n(n+1) / 2, illustrating the use of lemmas.
• A coinductive proof of a behavioral property of a simple flag object.
• A coinductive proof of correctness of array-with-pointer implementation of stack.
• A large compiler correctness proof using both induction and coinduction, with complex specifications and many lemmas.

---

To the Links Project homepage.
For information on the CafeOBJ project, of which this is part.
To the UCSD Meaning and Computation Lab homepage.

---

3 May 1998