The proofs linked to this page are "

- 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